×

Sharpening constraint programming approaches for bit-vector theory. (English) Zbl 1489.68249

Salvagnin, Domenico (ed.) et al., Integration of AI and OR techniques in constraint programming. 14th international conference, CPAIOR 2017, Padua, Italy, June 5–8, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10335, 3-20 (2017).
Summary: We address the challenge of developing efficient constraint programming-based approaches for solving formulas over the quantifier-free fragment of the theory of bitvectors (BV), which is of paramount importance in software verification. We propose CP(BV), a highly efficient BV resolution technique built on carefully chosen anterior results sharpened with key original features such as thorough domain combination or dedicated labeling. Extensive experimental evaluations demonstrate that CP(BV) is much more efficient than previous similar attempts from the CP community, that it is indeed able to solve the majority of the standard verification benchmarks for bitvectors, and that it already complements the standard SMT approaches on several crucial (and industry-relevant) aspects, notably in terms of scalability w.r.t. bit-width, theory combination or intricate mix of non-linear arithmetic and bitwise operators. This work paves the way toward building competitive CP-based verification-oriented solvers.
For the entire collection see [Zbl 1364.68017].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

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). doi: 10.1007/978-3-642-12002-2_7 · Zbl 1284.68379 · doi:10.1007/978-3-642-12002-2_7
[2] Bardin, S., Herrmann, P.: OSMOSE: automatic structural testing of executables. Softw. Test. Verification Reliab. 21(1), 29–54 (2011) · Zbl 05890829 · doi:10.1002/stvr.423
[3] Barret, C., Dill, D., Levitt, J.: A decision procedure for bit-vector arithmetic. In: DAC (1998) · doi:10.1145/277044.277186
[4] 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). doi: 10.1007/978-3-642-22110-1_14 · Zbl 05940712 · doi:10.1007/978-3-642-22110-1_14
[5] Barrett, C., et al.: The SMT-LIB Standard: Version 2.0. Technical report (2010)
[6] Barrett, C.W., et al.: Satisfiability modulo theories. In: Handbook of Satisfiability (2009) · Zbl 1184.68461
[7] 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 · doi:10.1007/3-540-49059-0_14
[8] Bjørner, N.: Taking satisfiability to the next level with Z3. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 1–8. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31365-3_1 · Zbl 1358.68248 · doi:10.1007/978-3-642-31365-3_1
[9] Blanc, B., et al.: Handling state-machines specifications with GATeL. Electron. Notes Theor. Comput. Sci. 264(3), 3–17 (2010) · doi:10.1016/j.entcs.2010.12.011
[10] Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: 15th International Conference on VLSI Design (2002) · doi:10.1109/ASPDAC.2002.995022
[11] 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). doi: 10.1007/978-3-642-00768-2_16 · Zbl 05535631 · doi:10.1007/978-3-642-00768-2_16
[12] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A lazy and layered SMT(BV) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 547–560. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-73368-3_54 · Zbl 05216259 · doi:10.1007/978-3-540-73368-3_54
[13] Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358–372. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71209-1_28 · Zbl 1186.68281 · doi:10.1007/978-3-540-71209-1_28
[14] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-36742-7_7 · Zbl 1381.68153 · doi:10.1007/978-3-642-36742-7_7
[15] Clarke, E., Kroening, 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). doi: 10.1007/978-3-540-24730-2_15 · Zbl 1126.68470 · doi:10.1007/978-3-540-24730-2_15
[16] Collavizza, H., Rueher, M., Hentenryck, P.: CPBPV: a constraint-programming framework for bounded program verification. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 327–341. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-85958-1_22 · Zbl 05372888 · doi:10.1007/978-3-540-85958-1_22
[17] David, R., et al.: BINSEC/SE: A dynamic symbolic execution toolkit for binary-level analysis. In: SANER 2016 (2016)
[18] Dechter, R.: Constraint Processing. Morgan Kaufmann Publishers Inc., Massachusetts (2003) · Zbl 1057.68114
[19] Dijkstra, E.W.: A Discipline of Programming, vol. 1. Prentice-Hall Englewood Cliffs, New Jersey (1976) · Zbl 0368.68005
[20] Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). doi: 10.1007/978-3-319-08867-9_49 · Zbl 06349545 · doi:10.1007/978-3-319-08867-9_49
[21] 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). doi: 10.1007/978-3-540-24605-3_37 · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37
[22] Ferrandi, F., Rendine, M., Sciuto, D.: Functional verification for SystemC descriptions using constraint solving. In: Design, Automation and Test in Europe (2002) · doi:10.1109/DATE.2002.998382
[23] Feydy, T., Schutt, A., Stuckey, P.J.: Global difference constraint propagation for finite domain solvers. In: PPDP (2008) · Zbl 1382.68232 · doi:10.1145/1389449.1389478
[24] 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). doi: 10.1007/978-3-540-73368-3_52 · Zbl 1135.68472 · doi:10.1007/978-3-540-73368-3_52
[25] Godefroid, P.: Test generation using symbolic execution. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) FSTTCS, vol. 18, pp. 24–33. Schloss Dagstuhl, Germany (2012)
[26] Gotlieb, A.: TCAS software verification using constraint programming. Knowl. Eng. Rev. 27(3), 343–360 (2012) · doi:10.1017/S0269888912000252
[27] Gotlieb, A., Botella, B., Rueher, M.: Automatic test data generation using constraint solving techniques. In: ISSTA (1998) · Zbl 0983.68583 · doi:10.1145/271771.271790
[28] Gotlieb, A., Leconte, M., Marre, B.: Constraint Solving on Modular Integers (2010)
[29] Henzinger, T.A., et al.: Lazy abstraction. In: POPL (2002) · Zbl 1323.68374 · doi:10.1145/503272.503279
[30] Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer Publishing Company Incorporated, Heidelberg (2008) · Zbl 1149.68071
[31] Leconte, M., Berstel, B.: Extending a CP solver with congruences as domains for program verification. In: Trends in Constraint Programming (2010)
[32] Manolios, P., Vroon, D.: Efficient circuit to CNF conversion. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 4–9. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-72788-0_3 · Zbl 05527191 · doi:10.1007/978-3-540-72788-0_3
[33] Marre, B., Blanc, B.: Test selection strategies for Lustre descriptions in GaTeL. Electron. Notes Theor. Comput. Sci. 111, 93–111 (2005) · doi:10.1016/j.entcs.2004.12.010
[34] Marre, B., Michel, C.: Improving the floating point addition and subtraction constraints. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 360–367. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-15396-9_30 · Zbl 05803740 · doi:10.1007/978-3-642-15396-9_30
[35] McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). doi: 10.1007/11817963_14 · Zbl 1188.68196 · doi:10.1007/11817963_14
[36] Michel, L.D., Hentenryck, P.: Constraint satisfaction over bit-vectors. In: Milano, M. (ed.) CP 2012. LNCS, pp. 527–543. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-33558-7_39 · Zbl 06122862 · doi:10.1007/978-3-642-33558-7_39
[37] Millo, R.A.D., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Commun. Assoc. Comput. Mach. 22(5), 271–280 (1979) · Zbl 0455.68017
[38] Moskewicz, M.W., et al.: Chaff: engineering an efficient SAT solver. In: Design Automation Conference, DAC (2001) · doi:10.1145/378239.379017
[39] Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079
[40] Parthasarathy, G., et al.: An efficient finite-domain constraint solver for circuits. In: 41st Design Automation Conference (2004) · doi:10.1145/996566.996628
[41] Pelleau, M., Miné, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 434–454. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-35873-9_26 · Zbl 1426.68159 · doi:10.1007/978-3-642-35873-9_26
[42] Scott, J.D., Flener, P., Pearson, J.: Bounded strings for constraint programming. In: ICTAI (2013) · doi:10.1109/ICTAI.2013.155
[43] Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999) · Zbl 01935259 · doi:10.1109/12.769433
[44] Sülflow, A., et al.: Evaluation of SAT like proof techniques for formal verification of word level circuits. In: 8th IEEE Workshop on RTL and High Level Testing (2007)
[45] Vemuri, R., Kalyanaraman, R.: Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming. IEEE Trans. VLSI Syst. 3(2), 201–214 (1995) · doi:10.1109/92.386221
[46] Wang, W., Søndergaard, H., Stuckey, P.J.: A bit-vector solver with word-level propagation. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 374–391. Springer, Cham (2016). doi: 10.1007/978-3-319-33954-2_27 · Zbl 1475.68360 · doi:10.1007/978-3-319-33954-2_27
[47] Williams, N., Marre, B., Mouy, P.: On-the-fly generation of K-path tests for C functions. In: ASE 2004 (2004) · doi:10.1109/ASE.2004.1342749
[48] Zeng, Z., Ciesielski, M., Rouzeyre, B.: Functional test generation using constraint logic programming. In: 11th International Conference on Very Large Scale Integration of Systems-on-Chip (2001)
[49] Zeng, Z., Kalla, P., Ciesielski, M.: LPSAT: a unified approach to RTL satisfiability. In: 4th Conference on Design, Automation and Test in Europe (2001) · doi:10.1109/DATE.2001.915055
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.