@inproceedings{1a592dea86a14b8eb0f5c5c034e2e4a4,
title = "A modular integration of SAT/SMT solvers to Coq through proof witnesses",
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.",
author = "Michael Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and Laurent Th{\'e}ry and Benjamin Werner",
year = "2011",
month = jan,
day = "1",
doi = "10.1007/978-3-642-25379-9\_12",
language = "English",
isbn = "9783642253782",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "135--150",
booktitle = "Certified Programs and Proofs - First International Conference, CPP 2011, Proceedings",
note = "1st International Conference on Certified Programs and Proofs, CPP 2011 ; Conference date: 07-12-2011 Through 09-12-2011",
}