Automatic program instrumentation for automatic verification. (English) Zbl 07798103
Enea, Constantin (ed.) et al., Computer aided verification. 35th international conference, CAV 2023, Paris, France, July 17–22, 2023. Proceedings. Part III. Cham: Springer. Lect. Notes Comput. Sci. 13966, 281-304 (2023).
Summary: In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.
For the entire collection see [Zbl 1529.68047].
For the entire collection see [Zbl 1529.68047].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Afzal, M.; Chakraborty, S.; Chauhan, A.; Chimdyalwar, B.; Darke, P.; Gupta, A.; Kumar, S.; Babu M, C.; Unadkat, D.; Venkatesh, R., VeriAbs: verification by abstraction and test generation (competition contribution), Tools and Algorithms for the Construction and Analysis of Systems, 383-387 (2020), Cham: Springer, Cham · doi:10.1007/978-3-030-45237-7_25 |
| [2] | Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer (2016). doi:10.1007/978-3-319-49812-6 |
| [3] | Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.; Bjørner, N.; Voronkov, A., Lazy abstraction with interpolants for arrays, Logic for Programming, Artificial Intelligence, and Reasoning, 46-61 (2012), Heidelberg: Springer, Heidelberg · Zbl 1352.68141 · doi:10.1007/978-3-642-28717-6_7 |
| [4] | Amilon, J., Esen, Z., Gurov, D., Lidström, C., Rümmer, P.: Automatic program instrumentation for automatic verification (extended technical report). CoRR abs/2306.00004 (2023). doi:10.48550/arXiv.2306.00004 |
| [5] | Amilon, J., Esen, Z., Gurov, D., Lidström, C., Rümmer, P.: Artifact for the CAV 2023 paper “Automatic Program Instrumentation for Automatic Verification”, April 2023. doi:10.5281/zenodo.7875416 |
| [6] | Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017), available at www.SMT-LIB.org |
| [7] | Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. http://frama-c.com/acsl.html |
| [8] | Beyer, D., Progress on software verification: SV-COMP 2022, Tools and Algorithms for the Construction and Analysis of Systems, 375-402 (2022), Cham: Springer, Cham · doi:10.1007/978-3-030-99527-0_20 |
| [9] | Beyer, D.: SV-Benchmarks: Benchmark Set for Software Verification and Testing (SV-COMP 2022 and Test-Comp 2022), January 2022. doi:10.5281/zenodo.5831003 |
| [10] | Beyer, D.; Dangl, M.; Wendler, P.; Kroening, D.; Păsăreanu, CS, Boosting k-induction with continuously-refined invariants, Computer Aided Verification, 622-640 (2015), Cham: Springer, Cham · doi:10.1007/978-3-319-21690-4_42 |
| [11] | Beyer, D.; Keremoglu, ME; Gopalakrishnan, G.; Qadeer, S., CPAchecker: a tool for configurable software verification, Computer Aided Verification, 184-190 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-22110-1_16 |
| [12] | Bjørner, N.; Gurfinkel, A.; McMillan, K.; Rybalchenko, A.; Beklemishev, LD; Blass, A.; Dershowitz, N.; Finkbeiner, B.; Schulte, W., Horn clause solvers for program verification, Fields of Logic and Computation II, 24-51 (2015), Cham: Springer, Cham · Zbl 1465.68044 · doi:10.1007/978-3-319-23534-9_2 |
| [13] | Bjørner, N.; McMillan, K.; Rybalchenko, A.; Logozzo, F.; Fähndrich, M., On solving universally quantified horn clauses, Static Analysis, 105-125 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-38856-9_8 |
| [14] | Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). doi:10.1007/978-3-319-10575-8 · Zbl 1390.68001 |
| [15] | Cuoq, P.; Kirchner, F.; Kosmatov, N.; Prevosto, V.; Signoles, J.; Yakobowski, B.; Eleftherakis, G.; Hinchey, M.; Holcombe, M., Frama-C-A software analysis perspective, Software Engineering and Formal Methods, 233-247 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-33826-7_16 |
| [16] | Daca, P.; Henzinger, TA; Kupriyanov, A.; Chaudhuri, S.; Farzan, A., Array folds logic, Computer Aided Verification, 230-248 (2016), Cham: Springer, Cham · Zbl 1411.68061 · doi:10.1007/978-3-319-41540-6_13 |
| [17] | De Angelis, E., Proietti, M., Fioravanti, F., Pettorossi, A.: Verifying catamorphism-based contracts using constrained Horn clauses. Theory Pract. Log. Program. 22(4), 555-572 (2022). doi:10.1017/S1471068422000175’ · Zbl 1541.68103 |
| [18] | Donaldson, AF; Kroening, D.; Rümmer, P.; Esparza, J.; Majumdar, R., Automatic analysis of scratch-pad memory code for heterogeneous multicore processors, Tools and Algorithms for the Construction and Analysis of Systems, 280-295 (2010), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-12002-2_24 |
| [19] | Ernst, G.: Korn - software verification with Horn clauses (competition contribution). In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13994, pp. 559-564. Springer (2023). doi: doi:10.1007/978-3-031-30820-8_36 |
| [20] | Esen, Z., Rümmer, P.: TriCera: Verifying C programs using the theory of heaps. In: 2022 Formal Methods in Computer Aided Design, FMCAD 2022, Trento, Italy, October 17 - October 21, 2022 (2022) (To appear) |
| [21] | Fedyukovich, G.; Prabhu, S.; Madhukar, K.; Gupta, A.; Dillig, I.; Tasiran, S., Quantified invariants via syntax-guided synthesis, Computer Aided Verification, 259-277 (2019), Cham: Springer, Cham · doi:10.1007/978-3-030-25540-4_14 |
| [22] | Filliâtre, J., Gondelman, L., Paskevich, A.: The spirit of ghost code. Formal Methods Syst. Des. 48(3), 152-174 (2016). doi:10.1007/s10703-016-0243-x · Zbl 1358.68070 |
| [23] | Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Hankin, C., Schmidt, D. (eds.) Proceedings of: Symposium on Principles of Programming Languages (POPL’01), pp. 193-205. ACM (2001). doi:10.1145/360204.360220 · Zbl 1323.68372 |
| [24] | Garg, P.; Löding, C.; Madhusudan, P.; Neider, D.; Sharygina, N.; Veith, H., Learning universally quantified invariants of linear data structures, Computer Aided Verification, 813-829 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_57 |
| [25] | Georgiou, P., Gleiss, B., Kovács, L.: Trace logic for inductive loop reasoning. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pp. 255-263. IEEE (2020). doi:10.34727/2020/isbn.978-3-85448-042-6_33 |
| [26] | Gurfinkel, A.; Kahsai, T.; Komuravelli, A.; Navas, JA; Kroening, D.; Păsăreanu, CS, The SeaHorn verification framework, Computer Aided Verification, 343-361 (2015), Cham: Springer, Cham · doi:10.1007/978-3-319-21690-4_20 |
| [27] | Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248-266. Springer, Cham (2018). doi:10.1007/978-3-030-01090-4_15 · Zbl 1517.68239 |
| [28] | Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009) · Zbl 1178.03001 |
| [29] | Henzinger, TA; Hottelier, T.; Kovács, L.; Rybalchenko, A.; Fermüller, CG; Voronkov, A., Aligators for arrays (tool paper), Logic for Programming, Artificial Intelligence, and Reasoning, 348-356 (2010), Heidelberg: Springer, Heidelberg · Zbl 1306.68143 · doi:10.1007/978-3-642-16242-8_25 |
| [30] | Hojjat, H., Rümmer, P.: The ELDARICA Horn solver. In: FMCAD 2018. pp. 1-7 (2018). doi:10.23919/FMCAD.2018.8603013 |
| [31] | K., H.G.V., Shoham, S., Gurfinkel, A.: Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL), 1-29 (2022). doi:10.1145/3498722 |
| [32] | Kahsai, T., Kersten, R., Rümmer, P., Schäf, M.: Quantified heap invariants for object-oriented programs. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017. EPiC Series in Computing, vol. 46, pp. 368-384. EasyChair (2017). http://easychair.org/publications/paper/Pmh · Zbl 1403.68126 |
| [33] | Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, The Kluwer International Series in Engineering and Computer Science, vol. 523, pp. 175-188. Springer (1999). doi:10.1007/978-1-4615-5229-1_12 |
| [34] | Leino, KRM; Clarke, EM; Voronkov, A., Dafny: an automatic program verifier for functional correctness, Logic for Programming, Artificial Intelligence, and Reasoning, 348-370 (2010), Heidelberg: Springer, Heidelberg · Zbl 1253.68095 · doi:10.1007/978-3-642-17511-4_20 |
| [35] | Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Shin, S.Y., Ossowski, S. (eds.) Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), Honolulu, Hawaii, USA, March 9-12, 2009, pp. 615-622. ACM (2009). doi:10.1145/1529282.1529411 |
| [36] | Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. ACM Trans. Program. Lang. Syst. 43(4), 15:1-15:54 (2021). 10.1145/3462205 · Zbl 1508.68071 |
| [37] | Monniaux, D.; Gonnord, L.; Rival, X., Cell morphing: from array programs to array-free horn clauses, Static Analysis, 361-382 (2016), Heidelberg: Springer, Heidelberg · Zbl 1394.68081 · doi:10.1007/978-3-662-53413-7_18 |
| [38] | Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403-435 (2004). doi:10.1145/1013560.1013562 · Zbl 1367.68175 |
| [39] | Priya, S.; Zhou, X.; Su, Y.; Vizel, Y.; Bao, Y.; Gurfinkel, A.; Hou, Z.; Ganesh, V., Verifying verified code, Automated Technology for Verification and Analysis, 187-202 (2021), Cham: Springer, Cham · doi:10.1007/978-3-030-88885-5_13 |
| [40] | Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pp. 55-74. IEEE Computer Society (2002). doi:10.1109/LICS.2002.1029817 |
| [41] | Segoufin, L.; Ésik, Z., Automata and logics for words and trees over an infinite alphabet, Computer Science Logic, 41-57 (2006), Heidelberg: Springer, Heidelberg · Zbl 1225.68103 · doi:10.1007/11874683_3 |
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.
