Formal Methods in System Design

, Volume 42, Issue 1, pp 3–23 | Cite as

Efficiently solving quantified bit-vector formulas

  • Christoph M. Wintersteiger
  • Youssef Hamadi
  • Leonardo de Moura
Article

Abstract

In recent years, bit-precise reasoning has gained importance in hardware and software verification. Of renewed interest is the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantifier-free fragment of bit-vector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bit-vector formulas to avoid an exponential blow-up during construction. Solvers for quantified formulas usually flatten the input to obtain a quantified Boolean formula, losing much of the word-level information in the formula. We present a new approach based on a set of effective word-level simplifications that are traditionally employed in automated theorem proving, heuristic quantifier instantiation methods used in SMT solvers, and model finding techniques based on skeletons/templates. Experimental results on two different types of benchmarks indicate that our method outperforms the traditional flattening approach by multiple orders of magnitude of runtime.

Keywords

Theorem proving Satisfiability SMT Bit-vectors QBF 

References

  1. 1.
    Barrett C, Stump A, Tinelli C (2010) The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org
  2. 2.
    Barrett C, Tinelli C (2007) CVC3. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin Google Scholar
  3. 3.
    Benedetti M (2005) Evaluating QBFs via symbolic skolemization. In: Proceedings of LPAR. LNCS, vol 3452. Springer, Berlin Google Scholar
  4. 4.
    Biere A (2005) Resolve and expand. In: Proceedings of SAT. LNCS, vol 3542. Springer, Berlin Google Scholar
  5. 5.
    Brummayer R, Biere A (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: Proceedings of TACAS. LNCS, vol 5505. Springer, Berlin Google Scholar
  6. 6.
    Bruttomesso R, Cimatti A, Franzén A, Griggio A, Sebastiani R (2008) The MathSAT 4 SMT solver. In: Proceedings of CAV. LNCS, vol 5123. Springer, Berlin Google Scholar
  7. 7.
    Colón M (2005) Schema-guided synthesis of imperative programs by constraint solving. In: Proceedings of international symposium on logic based program synthesis and transformation. LNCS, vol 3573. Springer, Berlin Google Scholar
  8. 8.
    Cook B, Kroening D, Rümmer P, Wintersteiger CM (2010) Ranking function synthesis for bit-vector relations. In: Proceedings of TACAS. LNCS, vol 6015. Springer, Berlin Google Scholar
  9. 9.
    Egly U, Seidl M, Woltran S (2009) A solver for QBFs in negation normal form. Constraints 14(1) Google Scholar
  10. 10.
    Ganesh V, Dill DL (2007) A decision procedure for bit-vectors and arrays. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin Google Scholar
  11. 11.
    Ge Y, de Moura L (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Proceedings of CAV. LNCS, vol 5643. Springer, Berlin Google Scholar
  12. 12.
    Giunchiglia E, Narizzano M, Tacchella A (2004) QuBE++: an efficient QBF solver. In: Proceedings of FMCAD. LNCS, vol 3312. Springer, Berlin Google Scholar
  13. 13.
    Goultiaeva A, Iverson V, Bacchus F (2009) Beyond CNF: a circuit-based QBF solver. In: Proceedings of SAT. LNCS, vol 5584. Springer, Berlin Google Scholar
  14. 14.
    Gulwani S, Srivastava S, Venkatesan R (2009) Constraint-based invariant inference over predicate abstraction. In: Proceedings of VMCAI. LNCS, vol 5403. Springer, Berlin Google Scholar
  15. 15.
    Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press, Cambridge MATHCrossRefGoogle Scholar
  16. 16.
    Jain H, Kroening D, Sharygina N, Clarke EM (2008) Word-level predicate-abstraction and refinement techniques for verifying RTL verilog. IEEE Trans CAD Int Circuits Syst 27(2) Google Scholar
  17. 17.
    Jha S, Gulwani S, Seshia S, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of ICSE. ACM, New York Google Scholar
  18. 18.
    Jobstmann B, Bloem R (2006) Optimizations for LTL synthesis. In: Proceedings of FMCAD. IEEE, New York Google Scholar
  19. 19.
    Knuth DE, Bendix PB (1970) Simple word problems in universal algebra. In: Proceedings of conference on computational problems in abstract algebra. Pergamon, New York Google Scholar
  20. 20.
    Lewis HR (1980) Complexity results for classes of quantificational formulas. J Comput Syst Sci 21(3) Google Scholar
  21. 21.
    Lonsing F, Biere A (2010) Integrating dependency schemes in search-based QBF solvers. In: Proceedings of SAT. LNCS, vol 6175. Springer, Berlin Google Scholar
  22. 22.
    Manolios P, Srinivasan SK, Vroon D (2007) BAT: the bit-level analysis tool. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin Google Scholar
  23. 23.
    de Moura L, Bjørner N (2007) Efficient E-matching for SMT solvers. In: Proceedings of CADE. LNCS, vol 4603. Springer, Berlin Google Scholar
  24. 24.
    de Moura L, Bjørner N (2008) Z3: An efficient SMT solver. In: Proceedings of TACAS. LNCS, vol 4963. Springer, Berlin Google Scholar
  25. 25.
    Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of POPL. ACM, New York Google Scholar
  26. 26.
    Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: Proceedings of VMCAI. LNCS, vol 2937. Springer, Berlin Google Scholar
  27. 27.
    Solar-Lezama A, Jones CG, Bodík R (2008) Sketching concurrent data structures. In: Proceedings of PLDI. ACM, New York Google Scholar
  28. 28.
    Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: Proceedings of PLDI. ACM, New York Google Scholar
  29. 29.
    Srivastava S, Gulwani S, Foster JS (2010) From program verification to program synthesis. In: Proceedings of POPL. ACM, New York Google Scholar
  30. 30.
    Staber S, Bloem R (2007) Fault localization and correction with QBF. In: Proceedings of SAT. LNCS, vol 4501. Springer, Berlin Google Scholar
  31. 31.
    Turing A (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines Google Scholar
  32. 32.
    Wille R, Fey G, Große D, EggersglüßS, Drechsler R (2007) Sword: a SAT like prover using word level information. In: Proceedings of the international conference on VLSI of system-on-chip. IEEE, New York Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  • Christoph M. Wintersteiger
    • 1
  • Youssef Hamadi
    • 1
  • Leonardo de Moura
    • 2
  1. 1.Microsoft ResearchCambridgeUK
  2. 2.Microsoft ResearchRedmondUSA

Personalised recommendations