package coq-bdds

  1. Overview
  2. No Docs
BDD algorithms and proofs in Coq, by reflection

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. K
    Kumar Neeraj Verma

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.10.0.tar.gz
md5=9d8155b5718bc6032daf45451eda40d6

Description

Provides BDD algorithms running under Coq. (BDD are Binary Decision Diagrams.) Allows one to do classical validity checking by reflection in Coq using BDDs, can also be used to get certified BDD algorithms by extraction. First step towards actual symbolic model-checkers in Coq. See file README for operation.

Tags

keyword: BDD keyword: binary decision diagrams keyword: classical logic keyword: propositional logic keyword: validity keyword: satisfiability keyword: model checking keyword: reflection category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category: Miscellaneous/Extracted Programs/Decision procedures date: May-July 1999

Published: 07 Dec 2019

Dependencies (3)

  1. coq-int-map >= "8.10" & < "8.11~"
  2. coq >= "8.10" & < "8.11~"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None