Article

Fast LCF-Style proof reconstruction for z3

Authors:

Tjark WeberAuthors Info & Claims

ITP'10: Proceedings of the First international conference on Interactive Theorem Proving

Pages 179 - 194

https://doi.org/10.1007/978-3-642-14052-5_14

Published: 11 July 2010 Publication History

Abstract

The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent reconstruction of these proofs in the theorem provers Isabelle/HOL and HOL4 with particular focus on efficiency. Our highly optimized implementations outperform previous LCF-style proof checkers for SMT, often by orders of magnitude. Detailed performance data shows that LCF-style proof reconstruction can be faster than proof search in Z3.

References

[1]

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002).

[2]

Gordon, M.J.C., Pitts, A.M.: The HOL logic and system. In: Towards Verified Systems. Real-Time Safety Critical Systems Series, vol. 2, pp. 49-70. Elsevier, Amsterdam (1994).

[3]

Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Springer, Heidelberg (2008).

[4]

Collavizza, H., Gordon, M.: Integration of theorem-proving and constraint programming for software verification. Technical report, Laboratoire d'Informatique, Signaux et Systèmes de Sophia-Antipolis (2008).

[5]

Böhme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie -- An Interactive Prover-Backend for the Verifying C Compiler. J. Automated Reasoning 44(1-2), 111-144 (2010).

[6]

Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: 7th International Workshop on Satisfiability Modulo Theories, SMT '09 (2009).

[7]

de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008).

[8]

Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979).

[9]

de Moura, L.M., Bjørner, N.: Proofs and refutations, and Z3. In: Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings. vol. 418, CEUR-WS.org (2008).

[10]

Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2 (August 2006), http://combination.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30. pdf (retrieved January 21, 2010).

[11]

McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. Electronic Notes in Theoretical Computer Science 144(2), 43-51 (2006).

[12]

Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: A preliminary report. In: 6th International Workshop on Satisfiability Modulo Theories, SMT '08 (2008).

[13]

Fontaine, P., Marion, J.Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167-181. Springer, Heidelberg (2006).

[14]

Hurlin, C., Chaieb, A., Fontaine, P., Merz, S., Weber, T.: Practical proof reconstruction for first-order logic and set-theoretical constructions. In: Proceedings of the Isabelle Workshop 2007, Bremen, Germany, July 2007, pp. 2-13 (2007).

[15]

Böhme, S.: Proof reconstruction for Z3 in Isabelle/HOL. In: 7th International Workshop on Satisfiability Modulo Theories, SMT '09 (2009).

[16]

Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. Applied Logic 7(1), 26-40 (2009).

[17]

Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Design and Application of Strategies/Tactics in Higher Order Logics (STRATA '03), pp. 56-68 (2003); Number NASA/CP-2003-212448 in NASA Technical Reports.

[18]

Hurd, J.: Metis performance benchmarks, http://www.gilith.com/software/ metis/performance.html (retrieved January 21, 2010).

[19]

HOL88 contributors: HOL88 source code, http://www.ftp.cl.cam.ac.uk/ftp/ hvg/hol88/holsys.tar.gz (retrieved January 21, 2010).

[20]

Barrett, C., Deters, M., Oliveras, A., Stump, A.: 5th Annual Satisfiability Modulo Theories Competition. In: SMT-COMP '09 (2009), http://www.smtcomp.org/ 2009/.

[21]

Norrish, M.: Complete integer decision procedures as derived rules in HOL. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 71-86. Springer, Heidelberg (2003).

[22]

Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81-94. Springer, Heidelberg (2006).

[23]

Wenzel, M.: Parallel proof checking in Isabelle/Isar. In: ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (2009).

[24]

Amjad, H.: Data compression for proof replay. J. Automated Reasoning 41(3-4), 193-218 (2008).

Cited By

Feng NMarsso LChechik MFilkov VRay BZhou M(2024)Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational ObjectsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695522(1521-1532)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695522
Parthasarathy GDardinier TBonneau BMüller PSummers A(2024)Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification LanguageProceedings of the ACM on Programming Languages10.1145/36564388:PLDI(1510-1534)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656438
Feng NHu ABayless SIqbal STrentin PWhalen MPike LBackes J(2024)DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic TheoriesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_1(3-23)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57246-3_1
Show More Cited By

Fast LCF-Style proof reconstruction for z3

Recommendations

Integrating a SAT Solver with an LCF-style Theorem Prover

This paper describes the integration of a leading SAT solver with Isabelle/HOL, a popular interactive theorem prover. The SAT solver generates resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem ...
Soundness of Hoare's logic: an automated proof using LCF

This paper presents a natural deduction proof of Hoare's logic carried out by the Edinburgh LCF theorem prover. The emphasis is on the way Hoare's theory is presented to the LCF, which looks very much like an exposition of syntax and semantics to human ...
HOLCF = HOL + LCF

HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ITP'10: Proceedings of the First international conference on Interactive Theorem Proving

July 2010

494 pages

ISBN:3642140513

Editors:
Matt Kaufmann
Department of Computer Sciences, University of Texas, Austin, Talyor Hall 2.124, Austin, TX,
,
Lawrence C. Paulson
Computer Laboratory, University of Cambridge, Talyor Hall 2.124, Cambridge,, TX, UK

Sponsors

EPSRC: Engineering and Physical Sciences Research Council
CADE: CADE Inc.
NSF
Hewlett-Packard Corporation: Hewlett-Packard Corporation
ASL: Association for Symbolic Logic

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 July 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

35
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Feng NMarsso LChechik MFilkov VRay BZhou M(2024)Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational ObjectsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695522(1521-1532)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695522
Parthasarathy GDardinier TBonneau BMüller PSummers A(2024)Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification LanguageProceedings of the ACM on Programming Languages10.1145/36564388:PLDI(1510-1534)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656438
Feng NHu ABayless SIqbal STrentin PWhalen MPike LBackes J(2024)DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic TheoriesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_1(3-23)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57246-3_1
Torstensson OWeber T(2023)Hammering Floating-Point ArithmeticFrontiers of Combining Systems10.1007/978-3-031-43369-6_12(217-235)Online publication date: 20-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-43369-6_12
Lotz KKulczynski MNowotka DPoulsen DSchlichtkrull A(2023)Verified Verifying: SMT-LIB for Strings in IsabelleImplementation and Application of Automata10.1007/978-3-031-40247-0_15(206-217)Online publication date: 19-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-40247-0_15
Sadykov RMandrykin M(2022)Complete Decision Procedure for the Theory of Bounded Pointer ArithmeticProgramming and Computing Software10.1134/S036176882208002348:8(770-780)Online publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1134/S0361768822080023
Barbosa HReynolds AKremer GLachnitt HNiemetz ANötzli AOzdemir APreiner MViswanathan AViteri SZohar YTinelli CBarrett C(2022)Flexible Proof Production in an Industrial-Strength SMT SolverAutomated Reasoning10.1007/978-3-031-10769-6_3(15-35)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_3
Hance TLattuada AHawblitzel CHowell JJohnson RParno BLu SHowell J(2020)Storage systems are distributed systems (so verify them that way!)Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation10.5555/3488766.3488772(99-115)Online publication date: 4-Nov-2020
https://dl.acm.org/doi/10.5555/3488766.3488772
Bentkamp ABlanchette JKlakow D(2019)A Formal Proof of the Expressiveness of Deep LearningJournal of Automated Reasoning10.1007/s10817-018-9481-563:2(347-368)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9481-5
Allamigeon XKatz R(2019)A Formalization of Convex Polyhedra Based on the Simplex MethodJournal of Automated Reasoning10.1007/s10817-018-9477-163:2(323-345)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9477-1
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten