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.
Type de document :
Rapport
[Research Report] RR-3859, INRIA. 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00072797
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:58:02
Dernière modification le : vendredi 1 juin 2018 - 12:02:02
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:22:54

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

237

Téléchargements de fichiers

368