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.7.0.tar.gz
md5=0e838b0ee3ee927f736b9c7baf8e95b7

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: 11 Jan 2019

Dependencies (3)

  1. coq-int-map >= "8.7" & < "8.8~"
  2. coq >= "8.7" & < "8.8~"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None