×

zbMATH — the first resource for mathematics

Deciding bit-vector formulas with mcsat. (English) Zbl 06623516
Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40969-6/pbk; 978-3-319-40970-2/ebook). Lecture Notes in Computer Science 9710, 249-266 (2016).
Summary: The model-constructing satisfiability calculus (mcSAT) is a recently proposed generalization of propositional DPLL/CDCL for reasoning modulo theories. In contrast to most DPLL(T)-based SMT solvers, which carry out conflict-driven learning only on the propositional level, mcSAT calculi can also synthesise new theory literals during learning, resulting in a simple yet very flexible framework for designing efficient decision procedures. We present an mcSAT calculus for the theory of fixed-size bit-vectors, based on tailor-made conflict-driven learning that exploits both propositional and arithmetic properties of bit-vector operations. Our procedure avoids unnecessary bit-blasting and performs well on problems from domains like software verification, and on constraints over large bit-vectors.
For the entire collection see [Zbl 1337.68009].

MSC:
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bardin, S., Herrmann, P., Perroud, F.: An alternative to SAT-based approaches for bit-vectors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 84–98. Springer, Heidelberg (2010) · Zbl 1284.68379 · doi:10.1007/978-3-642-12002-2_7
[2] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011) · Zbl 05940712 · doi:10.1007/978-3-642-22110-1_14
[3] Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011) · Zbl 05940713 · doi:10.1007/978-3-642-22110-1_15
[4] Berdine, J., Cox, A., Ishtiaq, S., Wintersteiger, C.M.: Diagnosing abstraction failure for separation logic–based analyses. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 155–173. Springer, Heidelberg (2012) · Zbl 06070744 · doi:10.1007/978-3-642-31424-7_16
[5] Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC (1999) · doi:10.1109/DAC.1999.781333
[6] Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999) · doi:10.1007/3-540-49059-0_14
[7] Bjørner, N.S., Pichora, M.C.: Deciding fixed and non-fixed size bit-vectors. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 376–392. Springer, Heidelberg (1998) · doi:10.1007/BFb0054184
[8] 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) · Zbl 1350.68225 · doi:10.1007/978-3-642-25379-9_15
[9] Bradley, A.R.: sat-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011) · Zbl 1317.68109 · doi:10.1007/978-3-642-18275-4_7
[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) · Zbl 05535631 · doi:10.1007/978-3-642-00768-2_16
[11] Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: ICCAD. ACM (2009) · doi:10.1145/1687399.1687403
[12] Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002) · Zbl 1010.68766 · doi:10.1007/3-540-45657-0_29
[13] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013) · Zbl 1381.68153 · doi:10.1007/978-3-642-36742-7_7
[14] Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004) · Zbl 1126.68470 · doi:10.1007/978-3-540-24730-2_15
[15] Cyrluk, D., Möller, M.O., Rueß, H.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 60–71. Springer, Heidelberg (1997) · doi:10.1007/3-540-63166-6_9
[16] Dunn, S.J., Martello, G., Yordanov, B., Emmott, S., Smith, A.: Defining an essential transcriptional factor program for naive pluripotency. Science 344(6188), 1156–1160 (2014) · doi:10.1126/science.1248882
[17] Dutertre, B.: System description: Yices 1.0.10. In: SMT-COMP 2007 (2007)
[18] Froehlich, A., Kovasznai, G., Biere, A.: Efficiently solving bit-vector problems using model checkers. In: SMT Workshop (2013)
[19] Fröhlich, A., Kovásznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 378–390. Springer, Heidelberg (2013) · Zbl 1345.68172 · doi:10.1007/978-3-642-38536-0_33
[20] Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007) · Zbl 1135.68472 · doi:10.1007/978-3-540-73368-3_52
[21] Griggio, A.: Effective word-level interpolation for software verification. In: FMCAD. FMCAD Inc. (2011)
[22] 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) · Zbl 06349541 · doi:10.1007/978-3-319-08867-9_45
[23] Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reasoning 51(1), 79–108 (2013) · Zbl 1314.90053 · doi:10.1007/s10817-013-9281-x
[24] Kovásznai, G., Fröhlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: SMT. EPiC Series, vol. 20. EasyChair (2013) · Zbl 1345.68172
[25] Kovásznai, G., Veith, H., Fröhlich, A., Biere, A.: On the complexity of symbolic verification and decision problems in bit-vector logic. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part II. LNCS, vol. 8635, pp. 481–492. Springer, Heidelberg (2014) · Zbl 1426.68127 · doi:10.1007/978-3-662-44465-8_41
[26] Kroening, D.: Computing over-approximations with bounded model checking. In: BMC Workshop, vol. 144, January 2006 · Zbl 1272.68264 · doi:10.1016/j.entcs.2005.07.021
[27] McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) · Zbl 1278.68184 · doi:10.1007/978-3-540-45069-6_1
[28] Möller, M.O., Rueß, H.: Solving bit-vector equations. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 36–48. Springer, Heidelberg (1998) · doi:10.1007/3-540-49519-3_4
[29] de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379 · doi:10.1007/978-3-540-78800-3_24
[30] de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013) · Zbl 1426.68251 · doi:10.1007/978-3-642-35873-9_1
[31] 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) · Zbl 1326.68164 · doi:10.1145/1217856.1217859
[32] Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
[33] Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (1970), translated from Russian: Zapiski Nauchnykh Seminarov LOMI 8 (1968)
[34] Wille, R., Fey, G., Große, D., Eggersglüß, S., Drechsler, R.: SWORD: a SAT like prover using word level information. In: International Conference on Very Large Scale Integration of System-on-Chip (VLSI-SoC 2007). IEEE (2007) · doi:10.1109/VLSISOC.2007.4402478
[35] Yordanov, B., Wintersteiger, C.M., Hamadi, Y., Kugler, H.: SMT-based analysis of biological computation. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 78–92. Springer, Heidelberg (2013) · Zbl 06328614 · doi:10.1007/978-3-642-38088-4_6
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.