A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Michaël Armand 1 Germain Faure 2, 3 Benjamin Grégoire 1 Chantal Keller 2, 3, * Laurent Thery 1 Benjamin Werner 3, 2
* Auteur correspondant
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.
Type de document :
Communication dans un congrès
Jouannaud, Jean-Pierre and Shao, Zhong. CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. Springer, 7086, pp.135-150, 2011, Lecture notes in computer science - LNCS. 〈10.1007/978-3-642-25379-9_12〉
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00639130
Contributeur : Chantal Keller <>
Soumis le : mardi 20 mars 2012 - 14:16:40
Dernière modification le : jeudi 11 janvier 2018 - 17:01:02
Document(s) archivé(s) le : lundi 26 novembre 2012 - 11:35:31

Fichier

cpp11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Thery, et al.. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. Jouannaud, Jean-Pierre and Shao, Zhong. CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. Springer, 7086, pp.135-150, 2011, Lecture notes in computer science - LNCS. 〈10.1007/978-3-642-25379-9_12〉. 〈hal-00639130〉

Partager

Métriques

Consultations de la notice

494

Téléchargements de fichiers

347