HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Reflecting BDDs in Coq

Abstract : We propose an implementation and a proof of correctness of binary decision diagrams (BDDs), completely formalized in Coq. This not only shows that BDD algorithms are correct, but also yields a certified BDD algorithm running in Caml, using extraction, and even allows us to run BDD-based algorithms inside Coq itself, by reflection. The latter point paves the path for a smooth integration of symbolic model-checking in the Coq proof assistant. Extensive experimental results show that this approach works in practice, and is able to solve both relatively hard propositional problems and actual industrial hardware verification problems.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:58:02 AM
Last modification on : Friday, February 4, 2022 - 3:10:26 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:22:54 PM


  • HAL Id : inria-00072797, version 1



Kumar Neeraj Verma, Jean Goubault-Larrecq. Reflecting BDDs in Coq. [Research Report] RR-3859, INRIA. 2000. ⟨inria-00072797⟩



Record views


Files downloads