×

Efficiently solving quantified bit-vector formulas. (English) Zbl 1284.03212

Summary: 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.

MSC:

03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barrett C, Stump A, Tinelli C (2010) The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org
[2] Barrett C, Tinelli C (2007) CVC3. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin · Zbl 1277.68132
[3] Benedetti M (2005) Evaluating QBFs via symbolic skolemization. In: Proceedings of LPAR. LNCS, vol 3452. Springer, Berlin · Zbl 1108.68569
[4] Biere A (2005) Resolve and expand. In: Proceedings of SAT. LNCS, vol 3542. Springer, Berlin · Zbl 1122.68585
[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 · Zbl 1187.68168
[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
[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 · Zbl 1134.68345
[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 · Zbl 1284.68172
[9] Egly U, Seidl M, Woltran S (2009) A solver for QBFs in negation normal form. Constraints 14(1) · Zbl 1167.68054
[10] Ganesh V, Dill DL (2007) A decision procedure for bit-vectors and arrays. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin · Zbl 1135.68472
[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 · Zbl 1242.68280
[12] Giunchiglia E, Narizzano M, Tacchella A (2004) QuBE++: an efficient QBF solver. In: Proceedings of FMCAD. LNCS, vol 3312. Springer, Berlin · Zbl 1117.68488
[13] Goultiaeva A, Iverson V, Bacchus F (2009) Beyond CNF: a circuit-based QBF solver. In: Proceedings of SAT. LNCS, vol 5584. Springer, Berlin · Zbl 1247.68236
[14] Gulwani S, Srivastava S, Venkatesan R (2009) Constraint-based invariant inference over predicate abstraction. In: Proceedings of VMCAI. LNCS, vol 5403. Springer, Berlin · Zbl 1206.68087
[15] Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press, Cambridge · Zbl 1178.03001
[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)
[17] Jha S, Gulwani S, Seshia S, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of ICSE. ACM, New York
[18] Jobstmann B, Bloem R (2006) Optimizations for LTL synthesis. In: Proceedings of FMCAD. IEEE, New York
[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 · Zbl 0188.04902
[20] Lewis HR (1980) Complexity results for classes of quantificational formulas. J Comput Syst Sci 21(3) · Zbl 0471.03034
[21] Lonsing F, Biere A (2010) Integrating dependency schemes in search-based QBF solvers. In: Proceedings of SAT. LNCS, vol 6175. Springer, Berlin · Zbl 1306.68165
[22] Manolios P, Srinivasan SK, Vroon D (2007) BAT: the bit-level analysis tool. In: Proceedings of CAV. LNCS, vol 4590. Springer, Berlin
[23] de Moura L, Bjørner N (2007) Efficient E-matching for SMT solvers. In: Proceedings of CADE. LNCS, vol 4603. Springer, Berlin · Zbl 1213.68578
[24] de Moura L, Bjørner N (2008) Z3: An efficient SMT solver. In: Proceedings of TACAS. LNCS, vol 4963. Springer, Berlin
[25] Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of POPL. ACM, New York · Zbl 0686.68015
[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 · Zbl 1202.68109
[27] Solar-Lezama A, Jones CG, Bodík R (2008) Sketching concurrent data structures. In: Proceedings of PLDI. ACM, New York
[28] Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: Proceedings of PLDI. ACM, New York · Zbl 1206.68087
[29] Srivastava S, Gulwani S, Foster JS (2010) From program verification to program synthesis. In: Proceedings of POPL. ACM, New York · Zbl 1312.68068
[30] Staber S, Bloem R (2007) Fault localization and correction with QBF. In: Proceedings of SAT. LNCS, vol 4501. Springer, Berlin · Zbl 1214.94086
[31] Turing A (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines
[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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.