Efficient strategies for CEGAR-based model checking. (English) Zbl 1468.68131

Hajdu, Ákos; Micskei, Zoltán

J. Autom. Reasoning 64, No. 6, 1051-1091 (2020).

Summary: Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68V15	Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Keywords:

formal verification; abstraction; CEGAR; experimental evaluation

Software:

LTSmin; SMTInterpol; CPAchecker; UFO; SatAbs; KLEE; SLAM; Wolverine; z3; R; BLAST

References:

[1]	Albarghouthi, A.: Software verification with program-graph interpolation and abstraction. Ph.D. thesis, University of Toronto (2015)
[2]	Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 7358, pp. 672-678. Springer (2012)
[3]	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, 1, 63-109 (2014) · Zbl 1317.68107 · doi:10.1007/s10703-014-0209-9
[4]	Ball, T.: Formalizing counterexample-driven refinement with weakest preconditions. Tech. Rep. MSR-TR-2004-134, Microsoft Research (2004)
[5]	Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian abstraction for model checking C programs. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 2031, pp. 268-283. Springer (2001) · Zbl 0978.68540
[6]	Ball, T., Rajamani, S.: The Slam toolkit. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 2102, pp. 260-264. Springer (2001) · Zbl 0996.68560
[7]	Ball, T., Rajamani, S.: Generating abstract explanations of spurious counterexamples in C programs. Tech. Rep. MSR-TR-2002-09, Microsoft Research (2002)
[8]	Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (report on SV-COMP 2016). In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 9636, pp. 887-904. Springer (2016). 10.1007/978-3-662-49674-9_55
[9]	Beyer, D.: Software verification with validation of results. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 10206, pp. 331-349. Springer (2017) · Zbl 1360.68016
[10]	Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proceedings of the 2009 Conference on Formal Methods in Computer-Aided Design, pp. 25-32. IEEE (2009). 10.1109/FMCAD.2009.5351147
[11]	Beyer, D.; Dangl, M.; Wendler, P., A unifying view on SMT-based software verification, J. Autom. Reason., 60, 3, 299-335 (2018) · Zbl 1426.68041 · doi:10.1007/s10817-017-9432-6
[12]	Beyer, D.; Henzinger, TA; Jhala, R.; Majumdar, R., The software model checker Blast, Int. J. Softw. Tools Technol. Transf., 9, 5, 505-525 (2007) · doi:10.1007/s10009-007-0044-z
[13]	Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 4590, pp. 504-518. Springer (2007) · Zbl 1135.68466
[14]	Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 6806, pp. 184-190. Springer (2011)
[15]	Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 7793, pp. 146-162. Springer (2013)
[16]	Beyer, D., Löwe, S., Wendler, P.: Refinement selection. In: Model Checking Software, Lecture Notes in Computer Science, vol. 9232, pp. 20-38. Springer (2015)
[17]	Beyer, D., Löwe, S., Wendler, P.: Sliced path prefixes: an effective method to enable refinement selection. In: Formal Techniques for Distributed Objects, Components, and Systems, Lecture Notes in Computer Science, vol. 9039, pp. 228-243. Springer (2015)
[18]	Beyer, D.; Löwe, S.; Wendler, P., Reliable benchmarking: requirements and solutions, Int. J. Softw. Tools Technol. Transf., 21, 1-29 (2017) · doi:10.1007/s10009-017-0469-y
[19]	Beyer, D., Wendler, P.: Algorithms for software model checking: predicate abstraction vs. Impact. In: Proceedings of the Formal Methods in Computer Aided Design, pp. 106-113. IEEE (2012)
[20]	Biere, A.; Heule, M.; van Maaren, H., Handbook of Satisfiability (2009), Amsterdam: IOS press, Amsterdam · Zbl 1183.68568
[21]	Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Formal Methods in Programming and Their Applications, Lecture Notes in Computer Science, vol. 735, pp. 128-141. Springer (1993)
[22]	Bradley, AR; Manna, Z., The Calculus of Computation: Decision Procedures with Applications to Verification (2007), Berlin: Springer, Berlin · Zbl 1126.03001
[23]	Brückner, I., Dräger, K., Finkbeiner, B., Wehrheim, H.: Slicing abstractions. In: International Symposium on Fundamentals of Software Engineering, Lecture Notes in Computer Science, vol. 4767, pp. 17-32. Springer (2007) · Zbl 1141.68457
[24]	Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pp. 443-446. IEEE (2008). 10.1109/ASE.2008.69
[25]	Cabodi, G.; Loiacono, C.; Palena, M.; Pasini, P.; Patti, D.; Quer, S.; Vendraminetto, D.; Biere, A.; Heljanko, K.; Baumgartner, J., Hardware model checking competition 2014: an analysis and comparison of solvers and benchmarks, J. Satisf. Boolean Model. Comput., 9, 135-172 (2016)
[26]	Cabodi, G., Nocco, S., Quer, S.: Interpolation sequences revisited. In: 2011 Design, Automation and Test in Europe, pp. 1-6. IEEE (2011). 10.1109/DATE.2011.5763056
[27]	Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, pp. 209-224. USENIX Association (2008)
[28]	Cavada, R., Cimatti, A., Franzén, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing predicate abstractions by integrating BDDs and SMT solvers. In: Proceedings of the Formal Methods in Computer Aided Design, pp. 69-76. IEEE (2007). 10.1109/FMCAD.2007.18
[29]	Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Model Checking Software, Lecture Notes in Computer Science, vol. 7385, pp. 248-254. Springer (2012)
[30]	Cimatti, A., Griggio, A.: Software model checking via IC3. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 10806, pp. 277-293. Springer (2012)
[31]	Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50, 5, 752-794 (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643
[32]	Clarke, E.; Grumberg, O.; Long, DE, Model checking and abstraction, ACM Trans. Program. Lang. Syst., 16, 5, 1512-1542 (1994) · doi:10.1145/186025.186051
[33]	Clarke, E.; Grumberg, O.; Peled, D., Model Checking (1999), Cambridge: MIT Press, Cambridge
[34]	Clarke, E.; Gupta, A.; Strichman, O., SAT-based counterexample-guided abstraction refinement, IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 23, 7, 1113-1123 (2004) · doi:10.1109/TCAD.2004.829807
[35]	Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SatAbs: SAT-based predicate abstraction for ANSI-C. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 3440, pp. 570-574. Springer (2005) · Zbl 1087.68586
[36]	Czech, M., Hüllermeier, E., Jakobs, M.C., Wehrheim, H.: Predicting rankings of software verification tools. In: Proceedings of the 3rd ACM SIGSOFT International Workshop on Software Analytics, pp. 23-26. ACM (2017)
[37]	Demyanova, Y.; Pani, T.; Veith, H.; Zuleger, F., Empirical software metrics for benchmarking of verification tools, Form. Methods Syst. Des., 50, 2, 289-316 (2017) · Zbl 1360.68371 · doi:10.1007/s10703-016-0264-5
[38]	Dietsch, D., Heizmann, M., Musa, B., Nutz, A., Podelski, A.: Craig vs. Newton in software model checking. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pp. 487-497. ACM (2017). 10.1145/3106237.3106307
[39]	Ermis, E., Hoenicke, J., Podelski, A.: Splitting via interpolants. In: Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 7148, pp. 186-201. Springer (2012) · Zbl 1326.68091
[40]	Fernández Adiego, B.; Darvas, D.; Blanco Viñuela, E.; Tournier, JC; Bliudze, S.; Blech, JO; González Suárez, VM, Applying model checking to industrial-sized PLC programs, IEEE Trans. Ind. Inform., 11, 6, 1400-1410 (2015) · doi:10.1109/TII.2015.2489184
[41]	Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 1254, pp. 72-83. Springer (1997)
[42]	Hajdu, Á., Micskei, Z.: Supplementary material for the paper “Efficient strategies for CEGAR-based model checking” (2018). 10.5281/zenodo.1252784
[43]	Hajdu, Á., Tóth, T., Vörös, A., Majzik, I.: A configurable CEGAR framework with interpolation-based refinements. In: Formal Techniques for Distributed Objects, Components and Systems, Lecture Notes in Computer Science, vol. 9688, pp. 158-174. Springer (2016) · Zbl 1347.68226
[44]	Hart, PE; Nilsson, NJ; Raphael, B., A formal basis for the heuristic determination of minimum cost paths, IEEE Trans. Syst. Sci. Cybern., 4, 2, 100-107 (1968) · doi:10.1109/TSSC.1968.300136
[45]	Heizmann, M., Chen, Y.F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., Podelski, A.: Ultimate Automizer and the search for perfect interpolants. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 10806, pp. 447-451. Springer (2018)
[46]	Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 232-244. ACM (2004) · Zbl 1325.68147
[47]	Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 58-70. ACM (2002) · Zbl 1323.68374
[48]	Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Theory and Applications of Satisfiability Testing—SAT 2012, Lecture Notes in Computer Science, vol. 7317, pp. 157-171. Springer (2012) · Zbl 1273.68229
[49]	Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 9035, pp. 692-707. Springer (2015)
[50]	Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Amparore, E., Beccuti, M., Berthomieu, B., Ciardo, G., Dal Zilio, S., Liebke, T., Li, S., Meijer, J., Miner, A., Srba, J., Thierry-Mieg, Y., van de Pol, J., van Dirk, T., Wolf, K.: Complete results for the 2019 edition of the model checking contest. (2019) http://mcc.lip6.fr/2019/results.php
[51]	Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 6806, pp. 573-578. Springer (2011)
[52]	Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 4144, pp. 424-437. Springer (2006)
[53]	Leucker, M., Markin, G., Neuhäußer, M.: A new refinement strategy for CEGAR-based industrial model checking. In: Hardware and Software: Verification and Testing, Lecture Notes in Computer Science, vol. 9434, pp. 155-170. Springer (2015). 10.1007/978-3-319-26287-1_10
[54]	Löwe, S.: Effective approaches to abstraction refinement for automatic software verification. Ph.D. thesis, University of Passau (2017)
[55]	McMillan, K.L.: Applications of Craig interpolants in model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 3440, pp. 1-12. Springer (2005) · Zbl 1087.68597
[56]	McMillan, K.L.: Lazy abstraction with interpolants. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 4144, pp. 123-136. Springer (2006) · Zbl 1188.68196
[57]	de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 4963, pp. 337-340. Springer (2008) · Zbl 1133.68009
[58]	R Core Team: R: a language and environment for statistical computing. R Foundation for Statistical Computing, Vienna, Austria (2017). https://www.R-project.org/
[59]	Sallai, Gy., Hajdu, Á., Tóth, T., Micskei, Z.: Towards evaluating size reduction techniques for software model checking. In: Proceedings of the 5th International Workshop on Verification and Program Transformation, EPTCS, vol. 253, pp. 75-91. Open Publishing Association (2017)
[60]	Tóth, T., Hajdu, Á., Vörös, A., Micskei, Z., Majzik, I.: Theta: a framework for abstraction refinement-based model checking. In: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, pp. 176-179. FMCAD inc. (2017)
[61]	Tóth, T., Majzik, I.: Lazy reachability checking for timed automata with discrete variables. In: Model Checking Software, Lecture Notes in Computer Science, vol. 10869, pp. 235-254. Springer (2018) · Zbl 1508.68225
[62]	Tseitin, G.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning, Symbolic Computation, pp. 466-483. Springer (1983)
[63]	Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Formal Methods in Computer-Aided Design, pp. 1-8. IEEE (2009)
[64]	Wohlin, C.; Runeson, P.; Höst, M.; Ohlsson, MC; Regnell, B.; Wesslén, A., Experimentation in Software Engineering (2012), Berlin: Springer, Berlin · Zbl 1069.68547