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.7.0