coq-bdds

BDD algorithms and proofs in Coq, by reflection. 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.

opam install coq-bdds.8.5.0
homepage
https://github.com/coq-contribs/bdds
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/bdds/issues
dependencies
coq (>= 8.5 & < 8.6~) & coq-int-map = 8.5.0
source
https://github.com/coq-contribs/bdds/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-bdds/coq-bdds.8.5.0