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
* Corresponding author
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
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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00639130
Contributor : Chantal Keller <>
Submitted on : Tuesday, March 20, 2012 - 2:16:40 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Document(s) archivé(s) le : Monday, November 26, 2012 - 11:35:31 AM

File

cpp11.pdf
Files produced by the author(s)

Identifiers

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. CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩. ⟨hal-00639130⟩

Share

Metrics

Record views

647

Files downloads

689