Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Skolemization for Substructural Logics Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors

Authors : Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters

Published in: Logic for Programming, Artificial Intelligence, and Reasoning

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter There Is No Best -Normalization Strategy for Higher-Order Reasoners
next chapter Abstract Domains and Solvers for Sets Reasoning
Footnotes
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.
 
Literature
1.
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) CrossRef
2.
Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. In: All about Proofs, Proofs for All, pp. 23–44 (2015)
3.
4.
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)
5.
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) CrossRef
6.
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)CrossRef
7.
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) CrossRef
8.
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) CrossRef
9.
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)
10.
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) CrossRef
11.
Chen, J., Chugh, R., Swamy, N.: Type-preserving compilation of end-to-end verification of security enforcement. In: Programming Language Design and Implementation (2010)
12.
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) CrossRef
13.
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) CrossRef
14.
Ge, Y., Barrett, C.: Proof translation and SMT-LIB benchmark certification: a preliminary report. In: Workshop on Satisfiability Modulo Theories (2008)
15.
Griggio, A.: Effective word-level interpolation for software verification. In: Formal Methods in Computer-Aided Design (2011)
16.
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)
17.
18.
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)
19.
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages (2006)
20.
S. Lescuyer and S. Conchon. A Reflexive Formalization of a SAT Solver in Coq. In Theorem Proving in Higher Order Logics, 2008
21.
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)
22.
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) CrossRef
23.
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)MathSciNetCrossRef
24.
Oe, D., Reynolds, A., Stump, A.: Fast and flexible proof checking for SMT. In: Workshop on Satisfiability Modulo Theories (2009)
25.
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)
26.
Reynolds, A., Tinelli, C., Hadarean, L.: Certified interpolant generation for EUF. In: Workshop on Satisfiability Modulo Theories (2011)
27.
Robinson, J.A.: Logic: Form and Function: The Mechanization of Deductive Reasoning. Elsevier, New York (1980)
28.
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)MATHCrossRef
29.
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)
30.
31.
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)
Metadata
Title
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
Authors
Liana Hadarean
Clark Barrett
Andrew Reynolds
Cesare Tinelli
Morgan Deters
Copyright Year
2015
Publisher
Springer Berlin Heidelberg
Book
Logic for Programming, Artificial Intelligence, and Reasoning

Print ISBN: 978-3-662-48898-0

Electronic ISBN: 978-3-662-48899-7

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-662-48899-7_24

Premium Partner

    Image Credits