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.
This work was supported in part by the french ANR DECERT initiative.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Source code of the development, http://www.lix.polytechnique.fr/~keller/Recherche/smtcoq.html
SMT-LIB, http://www.smtlib.org
Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification. In: Kaufmann and Paulson [9], pp. 83–98
Barendregt, H., Barendsen, E.: Autarkic Computations in Formal Proofs. J. Autom. Reasoning 28(3), 321–336 (2002)
Besson, F.: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007)
Böhme, S., Weber, T.: Fast LCF-Style Proof Reconstruction for Z3. In: Kaufmann and Paulson [9], pp. 179–194
Dénès, M.: Coq with native compilation, https://github.com/maximedenes/native-coq
Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006)
Kaufmann, M., Paulson, L.C. (eds.): ITP 2010. LNCS, vol. 6172. Springer, Heidelberg (2010)
Lescuyer, S., Conchon, S.: Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 287–303. Springer, Heidelberg (2009)
McLaughlin, S., Barrett, C., Ge, Y.: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. ENTCS 144(2), 43–51 (2006)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL. J. ACM 53(6), 937–977 (2006)
Oe, D., Stump, A.: Extended Abstract: Combining a Logical Framework with an RUP Checker for SMT Proofs. In: Lahiri, S., Seshia, S. (eds.) Proceedings of the 9th International Workshop on Satisfiability Modulo Theories, Snowbird, USA (2011)
Tseitin, G.S.: On the complexity of proofs in propositional logics. Automation of Reasoning: Classical Papers in Computational Logic (1967-1970) 2 (1983)
Weber, T.: SAT-based Finite Model Generation for Higher-Order Logic. Ph.D. thesis, Institut für Informatik, Technische Universität München, Germany (April 2008), http://www.cl.cam.ac.uk/~tw333/publications/weber08satbased.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B. (2011). A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In: Jouannaud, JP., Shao, Z. (eds) Certified Programs and Proofs. CPP 2011. Lecture Notes in Computer Science, vol 7086. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25379-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-25379-9_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25378-2
Online ISBN: 978-3-642-25379-9
eBook Packages: Computer ScienceComputer Science (R0)