Skip to main content
Springer Nature Link
Log in

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

  • Conference paper
Certified Programs and Proofs (CPP 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7086))

Included in the following conference series:

  • 874 Accesses

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

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 52.74
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Source code of the development, http://www.lix.polytechnique.fr/~keller/Recherche/smtcoq.html

  2. SMT-LIB, http://www.smtlib.org

  3. 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

    Google Scholar 

  4. Barendregt, H., Barendsen, E.: Autarkic Computations in Formal Proofs. J. Autom. Reasoning 28(3), 321–336 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Böhme, S., Weber, T.: Fast LCF-Style Proof Reconstruction for Z3. In: Kaufmann and Paulson [9], pp. 179–194

    Google Scholar 

  7. Dénès, M.: Coq with native compilation, https://github.com/maximedenes/native-coq

  8. 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)

    Chapter  Google Scholar 

  9. Kaufmann, M., Paulson, L.C. (eds.): ITP 2010. LNCS, vol. 6172. Springer, Heidelberg (2010)

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. McLaughlin, S., Barrett, C., Ge, Y.: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. ENTCS 144(2), 43–51 (2006)

    MATH  Google Scholar 

  12. 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)

    Article  MathSciNet  MATH  Google Scholar 

  13. 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)

    Google Scholar 

  14. Tseitin, G.S.: On the complexity of proofs in propositional logics. Automation of Reasoning: Classical Papers in Computational Logic (1967-1970) 2 (1983)

    Google Scholar 

  15. 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

Download references

Author information

Authors and Affiliations

  1. INRIA, Sophia-Antipolis, France

    Michael Armand, Benjamin Grégoire & Laurent Théry

  2. INRIA - Saclay–Île-de-France at LIX, École Polytechnique, France

    Germain Faure, Chantal Keller & Benjamin Werner

Authors
  1. Michael Armand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Germain Faure
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Benjamin Grégoire
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Chantal Keller
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Benjamin Werner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Tsinghua University, FIT 3-603, 100084, Beijing, China

    Jean-Pierre Jouannaud

  2. Department of Computer Science, Yale University, 51 Prospect Street, 06520-8285, New Haven, CT, USA

    Zhong Shao

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation