Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] BDDs/MDDs in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] BDDs/MDDs in Coq


chronological Thread 
  • From: Kumar Neeraj Verma <verma AT in.tum.de>
  • To: Nestor Catano <catano AT cs.york.ac.uk>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] BDDs/MDDs in Coq
  • Date: Fri, 17 Sep 2004 13:34:14 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

Nestor Catano schrieb:


Hi,

Does anyone know of work on modelling BDDs (Binary Decision Diagrams) or
MDDs(Multivalued Decision Diagrams) in Coq or in any other
proof-assistant/prover ?

See the BDDS contribution http://coq.inria.fr/contribs/bdds.html which provides
BDD algorithms which can be run inside Coq, as well as proofs. The SMC development
http://coq.inria.fr/contribs/smc.html extends this by providing garbage collection and
model checking.

Another development is BDD http://coq.inria.fr/contribs/bdd.html which models BDDs as trees,
without sharing. Its goal is to show that BDDs of equivalent formulae are identical.

Regards,
Kumar Neeraj Verma




Archive powered by MhonArc 2.6.16.

Top of Page