A unifying view on SMT-based software verification. (English) Zbl 1426.68041

Beyer, Dirk; Dangl, Matthias; Wendler, Philipp

J. Autom. Reasoning 60, No. 3, 299-335 (2018); correction ibid. 65, No. 3, 461 (2021).

Summary: After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different “schools of thought” of software verification: bounded model checking, \(k\)-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPAchecker. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions.

MSC:

68N30	Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60	Specification and verification (program logics, model checking, etc.)

Keywords:

software verification; program analysis; bounded model checking; \(k\)-induction; Impact; lazy abstraction; predicate abstraction; SMT solving

Software:

CBMC; SLAM; SeaHorn; PKind; CPAchecker; LLBMC; SMACK; CTIGAR; UFO; ESBMC; BLAST

References:

[1]	Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading, MA (1986) · Zbl 1155.68020
[2]	Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Proceedings of TACAS, LNCS 7214, pp. 157-172. Springer (2012) · Zbl 1352.68140
[3]	Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Proceedings of CAV, LNCS 7358, pp. 672-678. Springer (2012) · Zbl 0329.68018
[4]	Alberti, F; Bruttomesso, R; Ghilardi, S; Ranise, S; Sharygina, N, An extension of lazy abstraction with interpolation for programs with arrays, Form. Methods Syst. Des., 45, 63-109, (2014) · Zbl 1317.68107
[5]	Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Slam and static driver verifier: technology transfer of formal methods inside microsoft. In: Proceedings of IFM, LNCS 2999, pp. 1-20. Springer (2004) · Zbl 1325.68145
[6]	Ball, T; Levin, V; Rajamani, SK, A decade of software model checking with SLAM, Commun. ACM, 54, 68-76, (2011)
[7]	Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Proceedings of TACAS, LNCS 2031, pp. 268-283. Springer (2001) · Zbl 0978.68540
[8]	Ball, T., Rajamani, S.K.: The Slam project: debugging system software via static analysis. In: Proceedings of POPL, pp. 1-3. ACM (2002) · Zbl 0329.68018
[9]	Beckert, B; Hähnle, R, Reasoning and verification: state of the art and current trends, IEEE Intell. Syst., 29, 20-29, (2014)
[10]	Beyer, D.: Software verification with validation of results (report on SV-COMP 2017). In: Proceedings of TACAS, LNCS 10206, pp. 331-349. Springer (2017)
[11]	Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proceedings of FMCAD, pp. 25-32. IEEE (2009)
[12]	Beyer, D., Dangl, M.: SMT-based software model checking: an experimental comparison of four algorithms. In: Proceedings of VSTTE, LNCS 9971, pp. 181-198. Springer (2016)
[13]	Beyer, D., Dangl, M., Wendler, P.: Boosting \(k\)-induction with continuously-refined invariants. In: Proceedings of CAV, LNCS 9206, pp. 622-640. Springer (2015)
[14]	Beyer, D., Dangl, M., Wendler, P.: Combining \(k\)-induction with continuously-refined invariants. Technical Report MIP-1503, University of Passau (January 2015). arXiv:1502.00096
[15]	Beyer, D; Henzinger, TA; Jhala, R; Majumdar, R, The software model checker blast, Int. J. Softw. Tools Technol. Transf., 9, 505-525, (2007)
[16]	Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proceedings of VMCAI, LNCS 4349, pp. 378-394. Springer (2007) · Zbl 1132.68333
[17]	Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of PLDI, pp. 300-309. ACM (2007)
[18]	Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Proceedings of CAV, LNCS 4590, pp. 504-518. Springer (2007) · Zbl 1135.68466
[19]	Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: Proceedings of ASE, pp. 29-38. IEEE (2008) · Zbl 1154.68079
[20]	Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Proceedings of CAV, LNCS 6806, pp. 184-190. Springer (2011)
[21]	Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proceedings of FMCAD, pp. 189-197. FMCAD (2010) · Zbl 0329.68018
[22]	Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proceedings of FASE, LNCS 7793, pp. 146-162. Springer (2013)
[23]	Beyer, D., Löwe, S., Wendler, P.: Benchmarking and resource measurement. In: Proceedings of SPIN, LNCS 9232, pp. 160-178. Springer (2015)
[24]	Beyer, D., Petrenko, A.K.: Linux driver verification. In: Proceedings of ISoLA, LNCS 7610, pp. 1-6. Springer (2012)
[25]	Beyer, D., Wendler, P.: Algorithms for software model checking: predicate abstraction vs. Impact. In: Proceedings of FMCAD, pp. 106-113. FMCAD (2012) · Zbl 0081.24402
[26]	Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS, LNCS 1579, pp. 193-207. Springer (1999)
[27]	Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Proceedings of CAV, LNCS 8559, pp. 831-848. Springer (2014)
[28]	Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of VMCAI, LNCS 6538, pp. 70-87. Springer (2011) · Zbl 1317.68109
[29]	Brain, M., Joshi, S., Kröning, D., Schrammel, P.: Safety verification and refutation by \(k\)-invariants and \(k\)-induction. In: Proceedings of SAS, LNCS 9291, pp. 145-161. Springer (2015) · Zbl 0081.24402
[30]	Brückner, I; Dräger, K; Finkbeiner, B; Wehrheim, H, Slicing abstractions, Fundam. Inform., 89, 369-392, (2008) · Zbl 1154.68079
[31]	Bryant, RE, Graph-based algorithms for Boolean function manipulation, IEEE Trans. Comput., 35, 677-691, (1986) · Zbl 0593.94022
[32]	Cimatti, A., Griggio, A.: Software model checking via IC3. In: Proceedings of CAV, LNCS 7358, pp. 277-293. Springer (2012)
[33]	Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Proceedings of TACAS, LNCS 8413, pp. 46-61. Springer (2014) · Zbl 1368.68245
[34]	Clarke, EM; Grumberg, O; Jha, S; Lu, Y; Veith, H, Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50, 752-794, (2003) · Zbl 1325.68145
[35]	Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proceedings of TACAS, LNCS 2988, pp. 168-176. Springer (2004) · Zbl 1126.68470
[36]	Colón, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Proceedings of CAV, LNCS 2725, pp. 420-432. Springer (2003) · Zbl 1278.68164
[37]	Cordeiro, L.C., Morse, J., Nicole, D., Fischer, B.: Context-bounded model checking with Esbmc 1.17 (competition contribution). In: Proceedings of TACAS, LNCS 7214, pp. 534-537. Springer (2012)
[38]	Craig, W, Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symb. Log., 22, 250-268, (1957) · Zbl 0081.24402
[39]	Cytron, R; Ferrante, J; Rosen, BK; Wegman, MN; Zadeck, FK, Efficiently computing static single assignment form and the control dependence graph, ACM Trans. Program. Lang. Syst., 13, 451-490, (1991)
[40]	Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Proceedings of OOPSLA, pp. 443-456. ACM (2013) · Zbl 1381.68057
[41]	Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using \(k\)-induction. In: Proceedings of SAS, LNCS 6887, pp. 351-368. Springer (2011)
[42]	Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proceedings of FMCAD, pp. 125-134. FMCAD Inc. (2011)
[43]	Ermis, E., Hoenicke, J., Podelski, A.: Splitting via interpolants. In: Proceedings of VMCAI, LNCS 7148, pp. 186-201. Springer (2012) · Zbl 1326.68091
[44]	Gadelha, MYR; Ismail, HI; Cordeiro, LC, Handling loops in bounded model checking of C programs via \(k\)-induction, Int. J. Softw. Tools Technol. Transf., 19, 97-114, (2017)
[45]	Ghilardi, S., Ranise, S.: Goal-directed invariant synthesis for model checking modulo theories. In: Proceedings of TABLEAUX, LNCS 5607, pp. 173-188. Springer (2009) · Zbl 1260.68230
[46]	Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4) (2010) · Zbl 1213.68379
[47]	Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Proceedings of CAV, LNCS 1254, pp. 72-83. Springer (1997)
[48]	Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: a framework for verifying C programs (competition contribution). In: Proceedings of TACAS, LNCS 9035, pp. 447-450. Springer (2015)
[49]	Hajdu, Á., Tóth, T., Vörös, A., Majzik, I.: A configurable CEGAR framework with interpolation-based refinements. In: Proceedings of FORTE, LNCS 9688, pp. 158-174. Springer (2016) · Zbl 1347.68226
[50]	Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Proceedings of SAS, LNCS 5673, pp. 69-85. Springer (2009) · Zbl 1248.68146
[51]	Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL, pp. 58-70. ACM (2002) · Zbl 1323.68374
[52]	Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Proceedings of SAT, LNCS 7317, pp. 157-171. Springer (2012) · Zbl 1273.68229
[53]	Jhala, R; Majumdar, R, Software model checking, ACM Comput. Surv., 41, 21:1-21:54, (2009)
[54]	Jovanovic, D., Dutertre, B.: Property-directed \(k\)-induction. In: Proceedings of FMCAD, pp. 85-92. IEEE (2016)
[55]	Kahsai, T., Tinelli, C.: PKind: a parallel \(k\)-induction based model checker. In: Proceedings of International Workshop on Parallel and Distributed Methods in Verification, EPTCS 72, pp. 55-62 (2011)
[56]	Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakharov, V.: Establishing Linux driver verification process. In: Proceedings of Ershov Memorial Conference, LNCS 5947, pp. 165-176. Springer (2009)
[57]	Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of POPL, pp. 194-206. ACM (1973) · Zbl 0309.68020
[58]	King, JC, Symbolic execution and program testing, Commun. ACM, 19, 385-394, (1976) · Zbl 0329.68018
[59]	Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Proceedings of CAV, LNCS 8044, pp. 846-862. Springer (2013)
[60]	McMillan, K.L.: Interpolation and SAT-based model checking. In: Proceedings of CAV, LNCS 2725, pp. 1-13. Springer (2003) · Zbl 1278.68184
[61]	McMillan, K.L.: Lazy abstraction with interpolants. In: Proceedings of CAV, LNCS 4144, pp. 123-136. Springer (2006) · Zbl 1188.68196
[62]	McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Proceedings of TACAS, LNCS 2619, pp. 2-17. Springer (2003) · Zbl 1031.68520
[63]	Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin (1999) · Zbl 0932.68013
[64]	Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Proceedings of CAV, LNCS 8559, pp. 106-113. Springer (2014)
[65]	Rocha, H., Ismail, H.I., Cordeiro, L.C., Barreto, R.S.: Model checking embedded C software using \(k\)-induction and invariants. In: Proceedings of SBESC, pp. 90-95. IEEE (2015)
[66]	Schrammel, P., Kroening, D.: 2LS for program analysis (competition contribution). In: Proceedings of TACAS, LNCS 9636, pp. 905-907. Springer (2016)
[67]	Schuppan, V; Biere, A, Liveness checking as safety checking for infinite state spaces, Electron. Notes Theor. Comput. Sci., 149, 79-96, (2006) · Zbl 1273.68240
[68]	Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proceedings of FMCAD, LNCS 1954, pp. 127-144. Springer (2000) · Zbl 0081.24402
[69]	Sinz, C., Merz, F., Falke, S.: Llbmc: A bounded model checker for Llvm’s intermediate representation (competition contribution). In: Proceedings of TACAS, LNCS 7214, pp. 542-544. Springer (2012)
[70]	Wahl, T.: The \(k\)-induction principle. Available at http://www.ccs.neu.edu/home/wahl/Publications/k-induction.pdf (2013)
[71]	Wendler, P.: CPAchecker with sequential combination of explicit-state analysis and predicate analysis (competition contribution). In: Proceedings of TACAS, LNCS 7795, pp. 613-615. Springer (2013)