Article

Rocket-fast proof checking for SMT solvers

Author:

Michał MoskalAuthors Info & Claims

TACAS'08/ETAPS'08: Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems

Pages 486 - 500

Published: 29 March 2008 Publication History

Abstract

Modern Satisfiability Modulo Theories (SMT) solvers are used in a wide variety of software and hardware verification applications. Proof producing SMT solvers are very desirable as they increase confidence in the solver and ease debugging/profiling, while allowing for scenarios like Proof-Carrying Code (PCC). However, the size of typical proofs generated by SMT solvers poses a problem for the existing systems, up to the point where proof checking consumes orders of magnitude more computer resources than proof generation. In this paper we show how this problem can be addressed using a simple term rewriting formalism, which is used to encode proofs in a natural deduction style. We formally prove soundness of our rules and evaluate an implementation of the term rewriting engine on a set of proofs generated from industrial benchmarks. The modest memory and CPU time requirements of the implementation allow for proof checking even on a small PDA device, paving a way for PCC on such devices.

References

[1]

Fx7 web page, http://nemerle.org/fx7/

[2]

Barrett, C., Berezin, S.: CVC Lite: A new implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515-518. Springer, Heidelberg (2004).

[3]

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science (2001).

Digital Library

[4]

Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant. In: Second Automated Formal Methods workshop series (AFM 2007), Atlanta, Georgia, USA (November 2007).

Digital Library

[5]

de Bruijn, N.G.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math. 34(5), 381-392 (1972).

[6]

de Moura, L., Bjorner, N.: Efficient E-matching for SMT solvers. In: Proceedings of the 21st International Conference on Automated Deduction (CADE-21), Springer, Heidelberg (to appear, 2007).

Digital Library

[7]

de Nivelle, H.: Implementing the clausal normal form transformation with proof generation. In: fourth workshop on the implementation of logics, Almaty, Kazachstan, University of Liverpool, University of Manchester, pp. 69-83 (2003).

[8]

de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Information and Computation 199(1), 24-54 (2005).

Digital Library

[9]

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

Digital Library

[10]

Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: Proceedings 2nd Annual IEEE Symp. on Logic in Computer Science, LICS 1987, Ithaca, NY, USA, June, 22-25, 1987, pp. 194-204. IEEE Computer Society Press, New York (1987).

[11]

Harvey, W., Stuckey, P.: A unit two variable per inequality integer constraint solver for constraint logic programming (1997).

[12]

McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In: Armando, A., Cimatti, A. (eds.) Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005), Edinburgh, Scotland, January 2006. Electronic Notes in Theoretical Computer Science, vol. 144(2), pp. 43-51. Elsevier, Amsterdam (2006).

Digital Library

[13]

Necula, G.C.: Proof-carrying code. In: Conference Record of POPL 1997: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997, pp. 106-119 (1997).

Digital Library

[14]

SMT-LIB: The Satisfiability Modulo Theories Library. http://www.smt-lib.org/

[15]

Stump, A., Dill, D.: Faster Proof Checking in the Edinburgh Logical Framework. In: 18th International Conference on Automated Deduction (2002).

Digital Library

[16]

Zeller, M., Stump, A., Deters, M.: A signature compiler for the Edinburgh Logical Framework. In: Proceedings of International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (2007).

Cited By

Katz GBarrett CTinelli CReynolds AHadarean LPiskac RTalupur M(2016)Lazy proofs for DPLL(T)-based SMT solversProceedings of the 16th Conference on Formal Methods in Computer-Aided Design10.5555/3077629.3077649(93-100)Online publication date: 3-Oct-2016
https://dl.acm.org/doi/10.5555/3077629.3077649
Hadarean LBarrett CReynolds ATinelli CDeters M(2015)Fine Grained SMT Proofs for the Theory ofźFixed-Width Bit-VectorsProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_24(340-355)Online publication date: 24-Nov-2015
https://dl.acm.org/doi/10.1007/978-3-662-48899-7_24
Blech JPérin M(2012)Generating Invariant-Based Certificates for Embedded SystemsACM Transactions on Embedded Computing Systems (TECS)10.1145/2220336.222034611:2(1-22)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.1145/2220336.2220346
Show More Cited By

Index Terms

Rocket-fast proof checking for SMT solvers

Index terms have been assigned to the content through auto-classification.

Recommendations

Fast and flexible proof checking for SMT
SMT '09: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories

Fast and flexible proof checking can be implemented for SMT using the Edinburgh Logical Framework with Side Conditions (LFSC). LFSC provides a declarative format for describing proof systems as signatures. We describe several optimizations for LFSC ...
Bounded model checking of software using SMT solvers instead of SAT solvers
SPIN'06: Proceedings of the 13th international conference on Model Checking Software

C Bounded Model Checking (CBMC) has proven to be a successful approach to automatic software analysis. The key idea is to (i) build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property ...
SMT proof checking using a logical framework

Producing and checking proofs from SMT solvers is currently the most feasible method for achieving high confidence in the correctness of solver results. The diversity of solvers and relative complexity of SMT over, say, SAT means that flexibility, as ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS'08/ETAPS'08: Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems

March 2008

518 pages

ISBN:3540787992

Editors:
C. R. Ramakrishnan
Stony Brook University, Department of Computer Science, Stony Brook, NY
,
Jakob Rehof
Universität Dortmund, Fachbereich Informatik, Dortmund, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 29 March 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
3
Total Downloads

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

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Katz GBarrett CTinelli CReynolds AHadarean LPiskac RTalupur M(2016)Lazy proofs for DPLL(T)-based SMT solversProceedings of the 16th Conference on Formal Methods in Computer-Aided Design10.5555/3077629.3077649(93-100)Online publication date: 3-Oct-2016
https://dl.acm.org/doi/10.5555/3077629.3077649
Hadarean LBarrett CReynolds ATinelli CDeters M(2015)Fine Grained SMT Proofs for the Theory ofźFixed-Width Bit-VectorsProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_24(340-355)Online publication date: 24-Nov-2015
https://dl.acm.org/doi/10.1007/978-3-662-48899-7_24
Blech JPérin M(2012)Generating Invariant-Based Certificates for Embedded SystemsACM Transactions on Embedded Computing Systems (TECS)10.1145/2220336.222034611:2(1-22)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.1145/2220336.2220346
Strub PSwamy NFournet CChen JField JHicks M(2012)Self-certificationProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2103656.2103723(571-584)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103656.2103723
Strub PSwamy NFournet CChen J(2012)Self-certificationACM SIGPLAN Notices10.1145/2103621.210372347:1(571-584)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103621.2103723
Oe DStump AOliver CClancy K(2012)versatProceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation10.1007/978-3-642-27940-9_24(363-378)Online publication date: 22-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-27940-9_24
Darbari AFischer BMarques-Silva J(2010)Industrial-strength certified SAT solving through verified SAT proof checkingProceedings of the 7th International colloquium conference on Theoretical aspects of computing10.5555/1881833.1881856(260-274)Online publication date: 1-Sep-2010
https://dl.acm.org/doi/10.5555/1881833.1881856
Oe DReynolds AStump ADutertre BStrichman O(2009)Fast and flexible proof checking for SMTProceedings of the 7th International Workshop on Satisfiability Modulo Theories10.1145/1670412.1670414(6-13)Online publication date: 2-Aug-2009
https://dl.acm.org/doi/10.1145/1670412.1670414
Stump ADeters MPetcher ASchiller TSimpson TAltenkirch TMillstein T(2009)Verified programming in GuruProceedings of the 3rd workshop on Programming languages meets program verification10.1145/1481848.1481856(49-58)Online publication date: 20-Jan-2009
https://dl.acm.org/doi/10.1145/1481848.1481856
Stump AOe DBarrett Cde Moura LBabic DGoel A(2008)Towards an SMT proof formatProceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning10.1145/1512464.1512470(27-32)Online publication date: 7-Jul-2008
https://dl.acm.org/doi/10.1145/1512464.1512470

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents