Skip to main content
SpringerLink
Log in

SMTCoq: Mixing Automatic and Interactive Proof Technologies

  • Chapter
  • First Online:
Proof Technology in Mathematics Research and Teaching

Part of the book series: Mathematics Education in the Digital Era ((MEDE,volume 14))

Abstract

SMTCoq is a plugin for the Coq interactive theorem prover to work in conjunction with automated theorem provers based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT), in an efficient and expressive way. As such, it allows one to formally establish, in a proof assistant, mathematical results relying on large combinatorial properties that require automatic Boolean reasoning. To this end, the huge SAT proofs coming from such problems can be safely checked in Coq and combined with standard mathematical Coq developments in a generic and modular way, for instance to obtain a formal proof of the Erdős Discrepancy Conjecture. To achieve this objective with the same degree of safety as Coq itself, SMTCoq communicates with SAT and SMT solvers that, in addition to a yes/no answer, can output traces of their internal proof search. The heart of SMTCoq is thus a certified, efficient and modular checker for such traces expressed in a format that can encompass most aspects of SMT reasoning. Preprocessors—that need not be certified—for proof traces coming from the state-of-the-art SMT solvers CVC4 and veriT and SAT solvers zChaff and Glucose are implemented. Coq can thus work in conjunction with widely used provers. From a proof assistant perspective, SMTCoq also provides a mechanism to let Coq users enjoy automation provided by external provers.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    SMTCoq is available at https://smtcoq.github.io.

  2. 2.

    This corresponds to proving the invariant of the merge loop stating that the array is sorted up to a certain point.

  3. 3.

    This format has been designed together with the veriT (Bouton et al., 2009) proof production engine.

  4. 4.

    This definition of a clause is more general than the usual one: a literal can be any formula, even containing logical connectives.

  5. 5.

    It corresponds to the certificate given by veriT, stable version of 2016.

  6. 6.

    The certificate given by veriT, stable version of 2016, contains 178 steps.

  7. 7.

    In Coq, one simply needs to assign the variables using the model and compute that the formula reduces to the true formula.

  8. 8.

    The native-coq branch of Coq is progressively being integrated into the main version.

  9. 9.

    This research is supported by Labex DigiCosme (project ANR11LABEX0045DIGICOSME) operated by ANR as part of the program «Investissement d’Avenir» Idex ParisSaclay (ANR11IDEX000302).

References

  • Allen, S. F., Constable, R. L., Eaton, R., Kreitz, C., & Lorigo, L. (2000). The Nuprl open logical environment. In D. A. McAllester (Ed.), Proceedings of Automated Deduction—CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, 17–20 June 2000 (Vol. 1831, pp. 170–176). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • 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: J.-P. Jouannaud & Z. Shao (pp. 135–150).

    Google Scholar 

  • Asperti, A., Ricciotti, W., Coen, C.S., & Tassi, E. (2011). The matita interactive theorem prover. In N. Bjørner & V. Sofronie-Stokkermans (Eds.), Proceedings of Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011 (Vol. 6803, pp. 64–69). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Barbosa, H. (2016). Efficient instantiation techniques in SMT (work in progress). In P. Fontaine, S. Schulz, & J. Urban (Eds.), Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, 2 July 2016, CEUR Workshop Proceedings (Vol. 1635, pp. 1–10). CEUR-WS.org.

    Google Scholar 

  • Brummayer, B., & Biere, A. (2009). Fuzzing and delta-debugging SMT solvers. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories (pp. 1–5). ACM.

    Google Scholar 

  • Bancerek, G., Bylinski, C., Grabowski, A., Kornilowicz, A., Matuszewski, R., Naumowicz, et al. (2015). Mizar: state-of-the-art and beyond. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe & V. Sorge (Eds.), Proceedings of Intelligent Computer Mathematics—International Conference, CICM 2015, Washington, DC, USA, 13–17 July 2015 (Vol. 9150, pp. 261–279). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., et al. (2011). CVC4. In G. Gopalakrishnan & S. Qadeer (Eds.), Proceedings of Computer Aided Verification—23rd International Conference, CAV 2011, Snowbird, UT, USA, 14–20 July 2011 (Vol. 6806, pp. 171–177). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Besson, F., Cornilleau, P.-E., & Pichardie, D. (2011). In J.-P. Jouannaud, & Z. Shao (Eds.), Modular SMT proofs for fast reflexive checking inside coq (pp. 151–166).

    Google Scholar 

  • Boespflug, M., Dénès, M., & Grégoire, B. (2011). In J.-P. Jouannaud, & Z. Shao (Eds.), Full reduction at full throttle (pp. 362–377).

    Google Scholar 

  • Barrett, C., de Moura, L. M., Ranise, S., Stump, A., & Tinelli, C. (2010). The SMT-LIB initiative and the rise of SMT—(HVC 2010 award talk). In S. Barner, I. G. Harris, D. Kroening, & O. Raz (Eds.), Hardware and Software: Verification and Testing—6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, 4–7 October 2010. Revised Selected Papers (Vol. 6504, p. 3). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Besson, F. (2006). Fast reflexive arithmetic tactics the linear case and beyond. In T. Altenkirch & C. McBride (Eds.), TYPES (Vol. 4502, pp. 48–62). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Besson, F., Fontaine, P., & Théry, L. (2011). A flexible proof format for SMT: A proposal. In PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving August 1, 2011 Affiliated with CADE 2011, 31 July–5 August 2011 Wrocław, Poland (pp. 15–26).

    Google Scholar 

  • Bachmair, L., & Ganzinger, H. (1998). Equational reasoning in saturation-based theorem proving. Automated deduction—A basis for applications (Vol. 1, pp. 353–397).

    Google Scholar 

  • Bonacina, M. P., Graham-Lengrand, S., & Shankar, N. (2018). Proofs in conflict-driven theory combination. In J. Andronick & A. P. Felty (Eds.), Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, 8-9 January 2018 (pp. 186–200). ACM.

    Google Scholar 

  • Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2009). Handbook of satisfiability (Vol. 185). Frontiers in Artificial Intelligence and Applications. IOS Press.

    Google Scholar 

  • Blanchette, J. C., Kaliszyk, C., Paulson, L. C., & Urban, J. (2016). Hammering towards QED. Journal of Formalized Reasoning, 9(1), 101–148.

    Google Scholar 

  • Boulmé, S., & Maréchal, A. (2017). Toward certification for free! Working paper or preprint, July 2017.

    Google Scholar 

  • Bouton, T., de Oliveira, D., Déharbe, D., & Fontaine, P. (2009). In R. A. Schmidt (Eds.), veriT: An open, trustable and efficient SMT-solver (pp. 151–156).

    Google Scholar 

  • Böhme, S. B., & Weber, T. (2010). Fast LCF-style proof reconstruction for Z3. In M. Kaufmann & L. C. Paulson (Eds.), ITP, (Vol. 6172, pp. 179–194). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Cruz-Filipe, L., & Schneider-Kamp, P. (2017). Formally proving the Boolean pythagorean triples conjecture. In T. Eiter & D. Sands (Eds.), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7–12 May 2017 (Vol. 46, pp. 509–522). EPiC Series in Computing. EasyChair.

    Google Scholar 

  • Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Protzenko, J., Rastogi, A., Swamy, N., et al. (2017). Implementing and proving the TLS 1.3 record layer. In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, 22–26 May 2017 (pp. 463–482). IEEE Computer Society.

    Google Scholar 

  • de Moura, L. M., & Bjørner, N. (2007). Efficient e-matching for SMT solvers. In F. Pfenning (Ed.), Proceedings of Automated Deduction—CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, 17–20 July 2007 (Vol. 4603, pp. 183–198). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • de Moura, L. M., & Bjørner, N. (2008). Z3: An efficient SMT solver. In C. R. Ramakrishnan & J. Rehof (Eds.), TACAS (Vol. 4963, pp. 337–340). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • de Moura, L., Kong, S., Avigad, J., van Doorn, F., & von Raumer, J. (2015). The lean theorem prover (system description). In A. P. Felty & Aart Middeldorp (Eds.), Proceedings of Automated Deduction—CADE-25—25th International Conference on Automated Deduction, Berlin, Germany, 1–7 August 2015 (Vol. 9195, pp. 378–388). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Ekici, B., Katz, G., Keller, C., Mebsout, A., Reynolds, A. J., & Tinelli, C. (2016). Extending SMTCoq, a certified checker for SMT (Extended Abstract). In J. Christian Blanchette & C. Kaliszyk (Eds.), Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, 1 July 2016 (Vol. 210, pp. 21–29). EPTCS.

    Google Scholar 

  • Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., et al. (2017). SMTCoq: A plug-in for integrating SMT solvers into Coq. In R. Majumdar & V. Kuncak (Eds.), Computer Aided Verification—29th International Conference, CAV 2017, Heidelberg, Germany, 24–28 July 2017, Proceedings, Part II (Vol. 10427, pp. 126–133). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Fournet, C., Keller, C., & Laporte, V. (2016). A certified compiler for verifiable computing. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27–July 1, 2016 (pp. 268–280). IEEE Computer Society.

    Google Scholar 

  • Fu, Z., Marhajan, Y., & Malik, S. (2007). zChaff. Research Web Page. Princeton University, USA, March 2007. http://www.princeton.edu/~chaff/zchaff.html.

  • Filliâtre, J.-C., & Paskevich, A. (2013). Why3—Where programs meet provers. In M. Felleisen & P. Gardner (Eds.), Proceedings of Programming Languages and Systems—22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, 16–24 March 2013 (Vol. 7792, pp. 125–128). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., et al. (2013). A machine-checked proof of the odd order theorem. In S. Blazy, C. Paulin-Mohring & D. Pichardie (Eds.), Proceedings of Interactive Theorem Proving—4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013 (Vol. 7998, pp. 163–179). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Grégoire, B., & Mahboubi, A. (2005). Proving equalities in a commutative ring done right in Coq. In J. Hurd & T. F. Melham (Eds.), TPHOLs (Vol. 3603, pp. 98–113). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Gonthier, G. (2007). The four colour theorem: Engineering of a formal proof. In D. Kapur (Ed.), Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, 15–17 December 2007. Revised and Invited Papers (Vol. 5081, p. 333). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Gordon, M. (2000). From LCF to HOL: A short history. In G. D. Plotkin, C. Stirling & M. Tofte (Eds.), Proof, language, and interaction, essays in honour of Robin Milner (pp. 169–186). The MIT Press.

    Google Scholar 

  • Harrison, J., et al. (1996). Formalized mathematics. Citeseer.

    Google Scholar 

  • Hales, T. C., Adams, M., Bauer, G., Dang, D. T., Harrison, J.,  Le Hoang, T., et al. (2015). A formal proof of the Kepler conjecture. CoRR. arXiv:abs/1501.02155.

  • Huet, G. P., & Herbelin, H. (2014). 30 years of research and development around coq. In S. Jagannathan & P. Sewell (Eds.), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, 20-21 January 2014 (pp. 249–250). ACM.

    Google Scholar 

  • Heule, M. J. H., Kullmann, O., & Marek, V. W. (2016). Solving and verifying the Boolean pythagorean triples problem via cube-and-conquer. In N. Creignou & D. Le Berre (Eds.), Proceedings of Theory and Applications of Satisfiability Testing—SAT 2016—19th International Conference, Bordeaux, France, 5–8 July 2016 (Vol. 9710, pp. 228–245). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Hurd, J. (2005). System description: The Metis proof tactic. In Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL) (pp. 103–104).

    Google Scholar 

  • Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., & Pichardie, D. (2015). A formally-verified C static analyzer. In S. K. Rajamani & D. Walker (Eds.), Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15–17 January 2015 (pp. 247–259). ACM.

    Google Scholar 

  • Jouannaud, J.-P. & Shao, Z. (Eds.). (2011). Proceedings of Certified Programs and Proofs—First International Conference, CPP 2011, Kenting, Taiwan, 7–9 December 2011 (Vol. 7086). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Konev, B., & Lisitsa, A. (2015). Computer-aided proof of erdős discrepancy properties. Artificial Intelligence, 224, 103–118.

    Article  Google Scholar 

  • Kaufmann, M., & Moore, J. S. (1996). ACL2: An industrial strength version of Nqthm. In Proceedings of the Eleventh Annual Conference on Computer Assurance, 1996. COMPASS’96, Systems Integrity, Software Safety, Process Security (pp. 23–34). IEEE.

    Google Scholar 

  • Kohlhase, M., & Rabe, F. (2016). QED reloaded: Towards a pluralistic formal library of mathematical knowledge. Journal of Formalized Reasoning, 9(1), 201–234.

    Google Scholar 

  • Lescuyer, S. (2011). Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et developpement d’une tactique reflexive pour la demonstration automatique en coq). Ph.D. thesis, University of Paris-Sud, Orsay, France.

    Google Scholar 

  • MacKenzie, D. (1995). The automation of proof: A historical and sociological exploration. IEEE Annals of the History of Computing, 17(3), 7–29.

    Article  Google Scholar 

  • Miller, D. (2013). Foundational proof certificates: Making proof universal and permanent. In A. Momigliano, B. Pientka & R. Pollack (Eds.), Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, 23 September 2013 (pp. 1–2). ACM.

    Google Scholar 

  • Norell, U. (2009). Dependently typed programming in Agda. In A. Kennedy & A. Ahmed (Eds.), Proceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, 24 January 2009 (pp. 1–2). ACM.

    Google Scholar 

  • Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL( ). Journal of the ACM, 53(6), 937–977.

    Article  Google Scholar 

  • Owre, S., Rushby, J. M., & Shankar, N. (1992). PVS: A prototype verification system. In D. Kapur (Ed.), Proceedings of Automated Deduction—CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, 15–18 June 1992 (Vol. 607, pp. 748–752). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Paulson, L. C., & Blanchette, J. C. (2010). Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In G. Sutcliffe, S. Schulz & E. Ternovska (Eds.), The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, 9 October 2011 (Vol. 2, pp. 1–11). EPiC Series in Computing. EasyChair.

    Google Scholar 

  • Parno, B., Howell, J., Gentry, C., & Raykova, M. (2013). Pinocchio: Nearly practical verifiable computation. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, 19-22 May 2013 (pp. 238–252). IEEE Computer Society.

    Google Scholar 

  • Riazanov, A., & Voronkov, A. (2002). The design and implementation of VAMPIRE. AI Communications, 15(2–3), 91–110.

    Google Scholar 

  • Saillard, R. (2015). Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique). Ph.D. thesis, Mines ParisTech, France.

    Google Scholar 

  • Schmidt, R. A. (Ed.). (2009). Proceedings of Automated Deduction—CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, 2–7 August 2009 (Vol. 5663). Lecture Notes in Computer Science. Springer.

    Google Scholar 

  • Schulz, S. (2013). System description: E 1.8. In K. McMillan, A. Middeldorp, & A. Voronkov (Eds.), Proceedings of the 19th LPAR, Stellenbosch (Vol. 8312). LNCS. Springer.

    Google Scholar 

  • Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., et al.: Dependent types and multi-monadic effects in F. In R. Bodík, R. Majumdar (Eds.), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016 (pp. 256–270). ACM.

    Google Scholar 

  • Silva, J. P. M., Lynce, I., & Malik, S. (2009). Conflict-driven clause learning SAT solvers. In Biere et al. (Ed.), (pp. 131–153).

    Google Scholar 

  • Stump, A. (2009). Proof checking technology for satisfiability modulo theories. Electronic Notes in Theoretical Computer Science, 228, 121–133.

    Article  Google Scholar 

  • Tseitin, G. (1970). On the complexity of proofs in propositional logics. Seminars in Mathematics, 8, 466–483.

    Google Scholar 

  • Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., & Wischnewski, P. (2009). SPASS version 3.5. In R. A. Schmidt (Ed.), (pp. 140–145).

    Google Scholar 

Download references

Acknowledgements

This work would be impossible without the help from past, present and future contributors of SMTCoq. Past and present contributors are Mikäl Armand, Clark Barett, Valentin Blot, Burak Ekici, Germain Faure, Benjamin Grégoire, Guy Katz, Tianyi Liang, Alain Mebsout, Andrew Reynolds, Laurent Théry, Cesare Tinelli and Benjamin Werner. Contributors to the certification of the Erdős Discrepancy Conjecture include Maxime Dénès and Pierre-Yves Strub.

The author thanks Véronique Benzaken and Évelyne Contejean for providing good feedback in the choice of the examples.

The author finally thanks the editors for their invitation to contribute to this book, and the reviewers and editors for their valuable feedback.

Author information

Authors and Affiliations

  1. LRI, University of Paris-Sud, CNRS UMR 8623, Université Paris-Saclay, Bât 650 Ada Lovelace Université Paris Sud, 91405, Orsay Cedex, France

    Chantal Keller

Authors
  1. Chantal Keller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Chantal Keller .

Editor information

Editors and Affiliations

  1. Ontario Institute for Studies in Education, University of Toronto, Toronto, ON, Canada

    Gila Hanna

  2. AG Didaktik, Fachbereich 3, Universität Bremen, Bremen, Germany

    David A. Reid

  3. Faculty of Education, Stellenbosch University, Stellenbosch, South Africa

    Michael de Villiers

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Keller, C. (2019). SMTCoq: Mixing Automatic and Interactive Proof Technologies. In: Hanna, G., Reid, D., de Villiers, M. (eds) Proof Technology in Mathematics Research and Teaching . Mathematics Education in the Digital Era, vol 14. Springer, Cham. https://doi.org/10.1007/978-3-030-28483-1_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-28483-1_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-28482-4

  • Online ISBN: 978-3-030-28483-1

  • eBook Packages: EducationEducation (R0)

Publish with us

Policies and ethics

Search

Navigation