Logic for reasoning about bugs in loops over data sequences (IFIL)

D. A. Kondrat'ev

Modelirovanie i analiz informacionnyh sistem, Tome 30 (2023) no. 3, pp. 214-233.

Résumé

Classic deductive verification is not focused on reasoning about program incorrectness. Reasoning about program incorrectness using formal methods is an important problem nowadays. Special logics such as Incorrectness Logic, Adversarial Logic, Local Completeness Logic, Exact Separation Logic and Outcome Logic have recently been proposed to address it. However, these logics have two disadvantages. One is that they are based on under-approximation approaches, while classic deductive verification is based on the over-approximation approach. One the other hand, the use of the classic approach requires defining loop invariants in a general case. The second disadvantage is that the use of generalized inference rules from these logics results in having to prove too complex formulas in simple cases. Our contribution is a new logic for solving these problems in the case of loops over data sequences. These loops are referred to as finite iterations. We call the proposed logic the Incorrectness Finite Iteration Logic (IFIL). We avoid defining invariants of finite iterations using a symbolic replacement of these loops with recursive functions. Our logic is based on special inference rules for finite iterations. These rules allow generating formulas with recursive functions corresponding to finite iterations. The validity of these formulas may indicate the presence of bugs in the finite iterations. This logic has been implemented in a new version of the C-lightVer system for deductive verification of C programs.

Détail

Keywords: deductive verification, Hoare logic, bug localization, program incorrectness, loop invariant, finite iteration, C-lightVer
Mots-clés : ACL2.

Bibliographie

[1] R. Hähnle, M. Huisman, “Deductive software verification: from pen-and-paper proofs to industrial tools”, Computing and software science, Lecture Notes in Computer Science, 10000, Springer, 2019, 345–373 | DOI | Zbl

[2] K. R. Apt, E.-R. Olderog, “Fifty years of Hoare’s logic”, Formal Aspects of Computing, 31:6 (2019), 751–807 | DOI | MR | Zbl

[3] K. R. Apt, E.-R. Olderog, “Assessing the success and impact of Hoare’s logic”, Theories of programming: the life and works of tony hoare, 2021, 41–76 | DOI | Zbl

[4] C. A. R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM, 12:10 (1969), 576–580 | DOI | MR | Zbl

[5] B. Möller, P. O’Hearn, T. Hoare, “On algebra of program correctness and incorrectness”, Relational and algebraic methods in computer science, Lecture Notes in Computer Science, 13027, Springer, 2021, 325–343 | DOI | MR

[6] Q. L. Le, A. Raad, J. Villard, J. Berdine, D. Dreyer, P. W. O’Hearn, “Finding real bugs in big programs with incorrectness logic”, Proceedings of the ACM on Programming Languages, 6, OOPSLA1 (2022), 1–27 | MR

[7] P. W. O’Hearn, “Incorrectness logic”, Proceedings of the ACM on Programming Languages, 4, POPL (2019), 1–32 | DOI

[8] A. Raad, J. Berdine, H. Dang, D. Dreyer, P. O’Hearn, J. Villard, “Local reasoning about the presence of bugs: incorrectness separation logic”, Computer aided verification, 12225 (2020), 225–252, Springer | MR | Zbl

[9] J. Vanegue, “Adversarial logic”, Static analysis, Lecture Notes in Computer Science, 13790, Springer, 2022, 422–448 | DOI | MR

[10] M. Milanese, F. Ranzato, “Local completeness logic on Kleene algebra with tests”, Static analysis, Lecture Notes in Computer Science, 13790, Springer, 2022, 350–371 | DOI | MR

[11] B. Bruni, R. Giacobazzi, R. Gori, F. Ranzato, “A correctness and incorrectness program logic”, Journal of the ACM, 70:2 (2023), 1–45 | DOI | MR

[12] P. Maksimović, C. Cronjäger, A. Lööw, J. Sutherland, P. Gardner, “Exact separation logic: towards bridging the gap between verification and bug-finding”, 37th european conference on object-oriented programming (ECOOP 2023), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, 19:1–19:27

[13] N. Zilberstein, D. Dreyer, A. Silva, “Outcome logic: a unifying foundation of correctness and incorrectness reasoning”, Proceedings of the ACM on Programming Languages, 7, OOPSLA1 (2023), 522–550 | DOI

[14] T. Dardinier, P. Müller, Hyper hoare logic: (Dis-)Proving program hyperproperties (extended version), 2023, arXiv: 2301.10037 | MR

[15] A. Humenberger, M. Jaroschek, L. Kovács, “Invariant generation for multi-path loops with polynomial assignments”, Verification, model checking, and abstract interpretation, Lecture Notes in Computer Science, 10747, Springer, 2018, 226–246 | DOI | MR | Zbl

[16] S. Chakraborty, A. Gupta, D. Unadkat, “Full-program induction: verifying array programs sans loop invariants”, International Journal on Software Tools for Technology Transfer, 24:5 (2022), 843–888 | DOI

[17] V. A. Nepomniaschy, “Symbolic method of verification of definite iterations over altered data structures”, Programming and Computer Software, 31:1 (2005), 1–9 | DOI | MR | Zbl

[18] V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhailov, A. V. Promskii, “Towards verification of c programs. C-light language and its formal semantics”, Programming and Computer Software, 28:6 (2002), 314–323 | DOI | MR

[19] V. A. Nepomniaschy, I. S. Anureev, A. V. Promskii, “Towards verification of c programs: axiomatic semantics of the C-kernel language”, Programming and Computer Software, 29:6 (2003), 338–350 | DOI | MR | Zbl

[20] I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, D. A. Kondratyev, “Automatic c program verification based on mixed axiomatic semantics”, Automatic Control and Computer Sciences, 48:7 (2014), 407–414 | DOI

[21] D. A. Kondratyev, V. A. Nepomniaschy, “Automation of c program deductive verification without using loop invariants”, Programming and Computer Software, 48:5 (2022), 331–346 | DOI | MR

[22] D. A. Kondratyev, A. V. Promsky, “The complex approach of the C-lightVer system to the automated error localization in c-programs”, Automatic Control and Computer Sciences, 54:7 (2020), 728–739 | DOI | MR

[23] J. S. Moore, “Milestones from the pure lisp theorem prover to ACL2”, Formal Aspects of Computing, 31:6 (2019), 699–732 | DOI | MR | Zbl

[24] D. A. Kondratyev, I. V. Maryasov, V. A. Nepomniaschy, “The automation of c program verification by the symbolic method of loop invariant elimination”, Automatic Control and Computer Sciences, 53:7 (2019), 653–662 | DOI | MR

[25] L. Zhang, B. L. Kaminski, “Quantitative strongest post: a calculus for reasoning about the flow of quantitative information”, Proceedings of the ACM on Programming Languages, 6, OOPSLA1 (2022), 1–29

[26] S. Dailler, D. Hauzar, C. Marché, Y. Moy, “Instrumenting a weakest precondition calculus for counterexample generation”, Journal of Logical and Algebraic Methods in Programming, 99 (2018), 97–113 | DOI | MR | Zbl

[27] B. Becker, C. B. Lourenço, C. Marché, “Explaining counterexamples with giant-step assertion checking”, Proceedings of the 6th workshop on formal integrated development environment, 2021, 82–88

[28] Q. L. Le, J. Sun, L. H. Pham, S. Qin, S2TD: a separation logic verifier that supports reasoning of the absence and presence of bugs, 2022, arXiv: 2209.09327

[29] T. Dardinier, G. Parthasarathy, P. Müller, “Verification-preserving inlining in automatic separation logic verifiers”, Proceedings of the ACM on Programming Languages, 7, OOPSLA1 (2023), 789–818 | DOI

[30] R. Könighofer, R. Toegl, R. Bloem, “Automatic error localization for software using deductive verification”, Hardware and software: verification and testing, Lecture Notes in Computer Science, 8855, Springer, 2014, 92–98 | DOI

[31] P. Baudin, F. Bobot, D. Bühler, L. Correnson, F. Kirchner, N. Kosmatov, A. Maroneze, V. Perrelle, V. Prevosto, J. Signoles, N. Williams, “The dogged pursuit of bug-free c programs: the Frama-C software analysis platform”, Communications of the ACM, 64:8 (2021), 56–68 | DOI

[32] M. R. Gadelha, F. Monteiro, L. Cordeiro, D. Nicole, “ESBMC v6.0: verifying c programs using $k$-induction and invariant inference”, Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science, 11429, Springer, 2019, 209–213 | DOI

[33] S. Löwe, “CPAchecker with explicit-value analysis based on CEGAR and interpolation”, Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science, 7795, Springer, 2013, 610–612 | DOI

[34] D. Beyer, T. Lemberger, “CPA-SymExec: efficient symbolic execution in CPAchecker”, Proceedings of the 33rd acm/ieee international conference on automated software engineering, 2018, 900–903 | DOI

[35] C. Cadar, M. Nowack, “KLEE symbolic execution engine in 2019”, International Journal on Software Tools for Technology Transfer, 23:6 (2021), 867–870 | DOI

[36] B. Jacobs, J. Kiniry, M. Warnier, “Java program verification challenges”, Formal methods for components and objects, Lecture Notes in Computer Science, 2852, Springer, 2003, 202–219 | DOI