coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] BDDs/MDDs in Coq, Nestor Catano
- Re: [Coq-Club] BDDs/MDDs in Coq, Kumar Neeraj Verma
Archive powered by MhonArc 2.6.16.