Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072797
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:58:02 AM
Last modification on : Friday, June 1, 2018 - 12:02:02 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:22:54 PM

Identifiers

  • HAL Id : inria-00072797, version 1

Collections

Citation

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

Share

Metrics

Record views

317

Files downloads

645