Abstract
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 well as performance, is a critical characteristic of a proof-checking solution for SMT. This paper describes such a solution, based on a Logical Framework with Side Conditions (LFSC). We describe the framework and show how it can be applied for flexible proof production and checking for two different SMT solvers, clsat and cvc3. We also report empirical results showing good performance relative to solver execution time.
Similar content being viewed by others
Notes
At http://clc.cs.uiowa.edu/lfsc/. The release’s README file clarifies a number of minor differences with the concrete syntax used in this paper.
A simple example of dependent types is the type of bit vectors of (positive integer) size n.
For simplicity, we limit the description here to a single mark per variable. In reality, there are 32 such marks, each with its own \(\textbf {\textsf {markvar}}\) command.
For instance ∀x:τ. ϕ can be represented as (forall λx:τ. ϕ) where forall is a constant of type (τ→formula)→formula. Then, quantifier instantiation reduces to (lambda-term) application.
Recall that the ! symbol in the concrete syntax stands for Π-abstraction.
A variable v is the pivot of a resolution application with resolvent c 1∨c 2 if the clauses resolved upon are c 1∨v and ¬v∨c 2.
Additional cases are omitted for the sake of brevity. A comprehensive list of rules can be found in the appendix of [39]
The hardest QF_IDL benchmarks in SMT-LIB have difficulty 5.
The results are publicly available at http://www.smt-exec.org under the SMT-EXEC job clsat- lfsc-2009.8.
The outlier above the dotted line is diamonds.18.10.i.a.u.smt.
Each of these benchmarks consists of an unsatisfiable quantifier-free LRA formula. QF_RDL is a sublogic of QF_LRA.
Details of these proof systems as well as proof excerpts can be found in [39].
The lfsc checker can be used either with compiled or with interpreted side condition code.
References
Armando A, Montovani J, Platania L (2006) Bounded model checking of software using SMT solvers instead of SAT solvers. In: Proceedings of the 13th international SPIN workshop on model checking of software (SPIN’06), Lecture notes in computer science, vol 3925. Springer, Berlin, pp 146–162
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, Lecture notes in computer science, vol 7086. Springer, Berlin, pp 135–150
Barnett M, yuh Evan Chang B, Deline R, Jacobs B, Leino KR (2006) Boogie: a modular reusable verifier for object-oriented programs. In: 4th international symposium on formal methods for components and objects, Lecture notes in computer science, vol 4111. Springer, Berlin, pp 364–387
Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol 185. IOS Press, Amsterdam, pp 825–885, chap 26
Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0. In: Gupta A, Kroening D (eds) Proceedings of the 8th international workshop on satisfiability modulo theories, Edinburgh, England. Available from www.smtlib.org
Barrett C, Tinelli C (2007) CVC3. In: Damm W, Hermanns H (eds) Proceedings of the 19th international conference on computer aided verification (CAV’07), Berlin, Germany, Lecture notes in computer science, vol 4590. Springer, Berlin, pp 298–302
Bauer L, Garriss S, McCune JM, Reiter MK, Rouse J, Rutenbar P (2005) Device-enabled authorization in the Grey system. In: Proceedings of the 8th information security conference (ISC’05), pp 431–445
Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin
Besson F, Fontaine P, Théry L (2011) A flexible proof format for SMT: a proposal. In: Fontaine P, Stump A (eds) Workshop on Proof eXchange for Theorem Proving (PxTP)
Bobot F, Filliâtre JC, Marché C, Paskevich A (2011) Why3: Shepherd your herd of provers. In: Boogie 2011: first international workshop on intermediate verification languages, Wrocław, Poland
Böhme S, Weber T (2010) Fast LCF-style proof reconstruction for Z3. In: Kaufmann M, Paulson L (eds) Interactive theorem proving, Lecture notes in computer science, vol 6172. Springer, Berlin, pp 179–194
Bouton T, Caminha B, De Oliveira D, Déharbe D, Fontaine P (2009) veriT: an open, trustable and efficient SMT-solver. In: Schmidt RA (ed) Proceedings of the 22nd international conference on automated deduction (CADE), CADE-22. Springer, Berlin, pp 151–156
Chen J, Chugh R, Swamy N (2010) Type-preserving compilation of end-to-end verification of security enforcement. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI). ACM, New York, pp 412–423
Clarke EM, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Form Methods Syst Des 19(1):7–34
Deharbe D, Fontaine P, Paleo BW (2011) Quantifier inference rules for SMT proofs. In: Workshop on proof exchange for theorem proving
Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB (2002) Extended static checking for Java. In: Proc ACM conference on programming language design and implementation, pp 234–245
Fontaine P, Marion JY, Merz S, Nieto LP, Tiu A (2006) Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Tools and algorithms for construction and analysis of systems (TACAS), Lecture notes in computer science, vol 3920. Springer, Berlin, pp 167–181
Ford J, Shankar N (2002) Formal verification of a combination decision procedure. In: Voronkov A (ed) 18th international conference on automated deduction (CADE), Lecture notes in computer science, vol 2392. Springer, Berlin, pp 347–362
Ge Y, Barrett C (2008) Proof translation and SMT-LIB benchmark certification: a preliminary report. In: Proceedings of international workshop on satisfiability modulo theories
Goel A, Krstić S, Tinelli C (2009) Ground interpolation for combined theories. In: Schmidt R (ed) Proceedings of the 22nd international conference on automated deduction (CADE), Lecture notes in artificial intelligence, vol 5663. Springer, Berlin, pp 183–198
Hagen G, Tinelli C (2008) Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Cimatti A, Jones R (eds) Proceedings of the 8th international conference on formal methods in computer-aided design, Portland, Oregon. IEEE, New York, pp 109–117
Harper R, Honsell F, Plotkin G (1993) A framework for defining logics. J ACM 40(1):143–184
Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: Tools and algorithms for the construction and analysis of systems (TACAS), Lecture notes in computer science, vol 3920. Springer, Berlin, pp 459–473
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In: Matthews J, Anderson T (eds) 22nd ACM symposium on operating systems principles (SOSP). ACM, New York, pp 207–220
Kothari N, Mahajan R, Millstein TD, Govindan R, Musuvathi M (2011) Finding protocol manipulation attacks. In: Keshav S, Liebeherr J, Byers JW, Mogul JC (eds) Proceedings of the ACM SIGCOMM 2011 conference on applications, technologies, architectures, and protocols for computer communications, pp 26–37
Lee D, Crary K, Harper R (2007) Towards a mechanized metatheory of standard ML. In: Proceedings of 34th ACM symposium on principles of programming languages. ACM, New York, pp 173–184
Leroy X (2006) Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Morrisett G, Jones SP (eds) 33rd ACM symposium on principles of programming languages. ACM, New York, pp 42–54
Lescuyer S, Conchon S (2008) A reflexive formalization of a SAT solver in Coq. In: Emerging trends of the 21st international conference on theorem proving in higher order logics (TPHOLs)
Marić F (2010) Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor Comput Sci 411:4333–4356
McMillan K (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr, Somenzi F (eds) Proceedings of computer aided verification, Lecture notes in computer science, vol 2725. Springer, Berlin, pp 1–13
Moskal M (2008) Rocket-fast proof checking for SMT solvers. In: Ramakrishnan C, Rehof J (eds) Tools and algorithms for the construction and analysis of systems (TACAS), Lecture notes in computer science, vol 4963. Springer, Berlin, pp 486–500
de Moura L, Bjørner N (2008) Proofs and refutations, and Z3. In: Konev B, Schmidt R, Schulz S (eds) 7th international workshop on the implementation of logics (IWIL)
Necula G (1997) Proof-carrying code. In: 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 106–119
Necula G, Lee P (1998) Efficient representation and validation of proofs. In: 13th annual IEEE symposium on logic in computer science, pp 93–104
Necula G, Rahul S (2001) Oracle-based checking of untrusted software. In: Proceedings of the 28th ACM symposium on principles of programming languages, pp 142–154
Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J ACM 53(6):937–977
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic, Lecture notes in computer science, vol 2283. Springer, Berlin
Oe D, Reynolds A, Stump A (2009) Fast and flexible proof checking for SMT. In: Dutertre B, Strichman O (eds) Proceedings of international workshop on satisfiability modulo theories
Reynolds A, Hadarean L, Tinelli C, Ge Y, Stump A, Barrett C (2010) Comparing proof systems for linear real arithmetic with LFSC. In: Gupta A, Kroening D (eds) Proceedings of international workshop on satisfiability modulo theories
Reynolds A, Tinelli C, Hadarean L (2011) Certified interpolant generation for EUF. In: Lahiri S, Seshia S (eds) Proceedings of the 9th international workshop on satisfiability modulo theories
Robinson J, Voronkov AE (2001) Handbook of automated reasoning. Elsevier, Amsterdam
Sebastiani R (2007) Lazy satisability modulo theories. J Satisfiability Boolean Model Comput 3(3–4): 141–224
Stump A (2008) Proof checking technology for satisfiability modulo theories. In: Abel A, Urban C (eds) Proceedings of the international workshop on logical frameworks and metalanguages: theory and practice (LFMTP)
Stump A, Dill D (2002) Faster proof checking in the Edinburgh logical framework. In: 18th international conference on automated deduction (CADE), pp 392–407
Stump A, Oe D (2008) Towards an SMT proof format. In: Barrett C, de Moura L (eds) Proceedings of international workshop on satisfiability modulo theories
Van Gelder A (2012) http://users.soe.ucsc.edu/~avg/ProofChecker/ProofChecker-fileformat.txt (accessed Jan 10, 2005)
Watkins K, Cervesato I, Pfenning F, Walker D (2002) A concurrent logical framework I: judgments and properties. Tech. Rep. CMU-CS-02-101. Carnegie Mellon University
Weber T, Amjad H (2009) Efficiently checking propositional refutations in HOL theorem provers. J Appl Log 7(1):26–40
Zee K, Kuncak V, Rinard MC (2009) An integrated proof language for imperative programs. In: Proceedings of the 2009 ACM SIGPLAN conference on programming language design and implementation (PLDI), pp 338–351
Zeller M, Stump A, Deters M (2007) Signature compilation for the Edinburgh logical framework. In: Schürmann C (ed) Workshop on logical frameworks and meta-languages: theory and practice (LFMTP)
Zhang L, Malik S (2002) The quest for efficient Boolean satisfiability solvers. In: Proceedings of 8th international conference on computer aided deduction (CADE)
Acknowledgements
We would like to thank Yeting Ge and Clark Barrett for their help translating cvc3’s proof format into LFSC. We also thank the anonymous referees for their thoughtful and detailed reviews whose suggestions have considerably helped us improve the presentation.
This work was partially supported by funding from the US National Science Foundation, under awards 0914877 and 0914956.
Author information
Authors and Affiliations
Corresponding author
Appendices
Appendix A: Typing rules for code
The completely standard type-computation rules for code terms are given in Fig. 21. Code terms are monomorphically typed. We write N for any arbitrary precision integer, and use several arithmetic operations on these; others can be easily modularly added. Function applications are required to be simply typed. In the typing rule for pattern matching expressions, patterns P must be of the form c or (c x 1 ⋯ x m ), where c is a constructor, not a bound variable (we do not formalize the machinery to track this difference). In the latter case, ctxt(P)={x 1:T 1,…x n :T n }, where c has type Πx 1:T 1.⋯x n :T n .T. We sometimes write (do C 1 C 2) as an abbreviation for (let x C 1 C 2), where \(x\not\in \hbox{\texttt{FV}}(C_{2})\).
Appendix B: Helper code for resolution
The helper code called by the side condition program resolve of the encoded resolution rule R is given in Figs. 22 and 23. We can note the frequent uses of match, for decomposing or testing the form of data. The program eqvar of Fig. 22 uses variable marking to test for equality of LF variables. The code assumes a datatype of Booleans tt and ff. It marks the first variable, and then tests if the second variable is marked. Assuming all variables are unmarked except during operations such as this, the second variable will be marked iff it happens to be the first variable. The mark is then cleared (recall that markvar toggles marks), and the appropriate Boolean result returned. Marks are also used by dropdups to drop duplicate literals from the resolvent.
Appendix C: Small example proof
Figure 24 shows a small QF_IDL proof. This proof derives a contradiction from the assumed formula
The proof begins by introducing the variables x, y, and z, and the assumption (named f) of the formula above. Then it uses CNF conversion rules to put that formula into CNF. CNF conversion starts with an application of the start rule, which turns the hypothesis of the input formula \((\mathsf{th\_hold}\ \phi)\) to a proof of the partial clause \((\mathsf{pc\_hold}\ (\phi;))\). The dist_pos, mentioned also in Sect. 4.3 above, breaks a conjunctive partial clause into conjuncts. The decl_atom_pos proof rule introduces new propositional variables for positive occurrences of atomic formulas. The new propositional variables introduced this way are v0, v1, and v2, corresponding to the atomic formulas (let us call them ϕ 0, ϕ 1, and ϕ 2) in the original assumed formula, in order. The decl_atom_pos rule is similar to rename (discussed in Sect. 4.3 above), but it also binds additional meta-variables of type (atom v ϕ) to record the relationships between variables and abstracted formulas. So for example, a0 is of type (atom v0 ϕ 0 ). The clausify rule turns the judgements of partial clauses with the empty formula sequence \((\mathsf{pc\_holds}\ (;c))\) to the judgements of pure propositional clauses (holds c). Here, this introduces variables x0, x1, and x2 as names for the asserted unit clauses ϕ 0, ϕ 1, and ϕ 2, respectively.
After CNF conversion is complete, the proof derives a contradiction from those asserted unit clauses and a theory clause derived using assume_true (see Sect. 4.4) from a theory contradiction. The theory contradiction is obtained with idl_trans and idl_contra (Sect. 5.1).
Rights and permissions
About this article
Cite this article
Stump, A., Oe, D., Reynolds, A. et al. SMT proof checking using a logical framework. Form Methods Syst Des 42, 91–118 (2013). https://doi.org/10.1007/s10703-012-0163-3
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-012-0163-3