Abstract
Many high-level verification tools rely on SMT solvers to efficiently discharge complex verification conditions. Some applications require more than just a yes/no answer from the solver. For satisfiable quantifier-free problems, a satisfying assignment is a natural artifact. In the unsatisfiable case, an externally checkable proof can serve as a certificate of correctness and can be mined to gain additional insight into the problem. We present a method of encoding and checking SMT-generated proofs for the quantifier-free theory of fixed-width bit-vectors. Proof generation and checking for this theory poses several challenges, especially for proofs based on reductions to propositional logic. Such reductions can result in large resolution subproofs in addition to requiring a proof that the reduction itself is correct. We describe a fine-grained proof system formalized in the LFSC framework that addresses some of these challenges with the use of computational side-conditions. We report results using a proof-producing version of the CVC4 SMT solver on unsatisfiable quantifier-free bit-vector benchmarks from the SMT-LIB benchmark library.
Work partially supported by DARPA award FA8750-13-2-0241 and ERC project 280053 (CPROVER).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
For example, the CVC4 code base consists of over 250 K lines of C++ code.
- 2.
For simplicity, we will ignore here the issue of whether the background theory is the combination of several more basic theories or not.
- 3.
This step typically also includes the application of simplifying rewrite rules, which we ignore in this paper. Extending the approach here to include the many pre-processing rewrite rules used in real solvers is tedious but straightforward.
- 4.
Intuitively, an LF expression of dependent type \(\varPi \varphi {:}\mathsf {form}.\,\mathsf {holds}(\varphi )\) represents a proof that the formula \(\varphi \) holds.
- 5.
Recall that \( bbAtom (a)\) is a propositional formula encoding the semantics of atom a, and contains \(\mathsf {bitOf} _i\) applications on the bit-vector variables in a.
- 6.
For details on how to use LFSC to encode proofs for CNF conversion, see [28].
- 7.
For simplicity, \(\mathsf {introUnit}\) only introduces literals in positive polarity. In reality, we also use a dual version that introduces literals in negative polarity.
- 8.
Experiments were run on the queue \(\mathsf {all.q}\) consisting of Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40 GHz machines with 268 GB of memory.
- 9.
CVC4 solved 26001 problems in that division compared to 26260 problems solved by the winning solver, Boolector [10].
- 10.
Overhead in each column is measured by comparing the time taken to solve only those problems solved by both the default and the column configuration.
References
Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011)
Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. In: All about Proofs, Proofs for All, pp. 23–44 (2015)
Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2015). www.SMT-LIB.org
Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Conference on Computer Aided Verification (2002)
Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 151–166. Springer, Heidelberg (2011)
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)
Böhme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 183–198. Springer, Heidelberg (2011)
Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179–194. Springer, Heidelberg (2010)
Bouton, T., Caminha, D., De Oliveira, B., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Conference on Automated Deduction (2009)
Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009)
Chen, J., Chugh, R., Swamy, N.: Type-preserving compilation of end-to-end verification of security enforcement. In: Programming Language Design and Implementation (2010)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
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., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006)
Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: a preliminary report. In: Workshop on Satisfiability Modulo Theories (2008)
Griggio, A.: Effective word-level interpolation for software verification. In: Formal Methods in Computer-Aided Design (2011)
Hadarean, L., Bansal, K., Jovanović, D., Barrett, C., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 680–695. Springer, Heidelberg (2014)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143–184 (1993)
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.: SeL4: formal verification of an OS kernel. In: Symposium on Operating Systems Principles (2009)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages (2006)
S. Lescuyer and S. Conchon. A Reflexive Formalization of a SAT Solver in Coq. In Theorem Proving in Higher Order Logics, 2008
McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: a case study combining HOL-Light and CVC lite. In: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005) (2006)
Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 486–500. Springer, Heidelberg (2008)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract davis-putnam-logemann-loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)
Oe, D., Reynolds, A., Stump, A.: Fast and flexible proof checking for SMT. In: Workshop on Satisfiability Modulo Theories (2009)
Reynolds, A., Hadarean, L., Tinelli, C., Ge, Y., Stump, A., Barrett, C.: Comparing proof systems for linear real arithmetic with LFSC. In: Workshop on Satisfiability Modulo Theories (2010)
Reynolds, A., Tinelli, C., Hadarean, L.: Certified interpolant generation for EUF. In: Workshop on Satisfiability Modulo Theories (2011)
Robinson, J.A.: Logic: Form and Function: The Mechanization of Deductive Reasoning. Elsevier, New York (1980)
Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods Syst. Des. 42(1), 91–118 (2013)
Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367–373. Springer, Heidelberg (2014)
Van, A.: Gelder. http://users.soe.ucsc.edu/avg/ProofChecker/ProofChecker-fileformat.txt
Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Heidelberg (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hadarean, L., Barrett, C., Reynolds, A., Tinelli, C., Deters, M. (2015). Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_24
Download citation
DOI: https://doi.org/10.1007/978-3-662-48899-7_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48898-0
Online ISBN: 978-3-662-48899-7
eBook Packages: Computer ScienceComputer Science (R0)