Логика для суждений об ошибках в циклах над последовательностями данных (IFIL)

Классическая дедуктивная верификация не ориентирована на доказательство некорректности программ. Доказательство некорректности программ с помощью формальных методов является актуальной задачей в настоящее время. Специальные логики, такие как Incorrectness Logic, Adversarial Logic, Local Completeness Logic, Exact Separation Logic и Outcome Logic, были недавно предложены для решения данной задачи. Но у данных логик имеется два недостатка. Во-первых, в данных логиках используются подходы, основанные на нижней аппроксимации, тогда как в классической дедуктивной верификации используется подход, основанный на верхней аппроксимации. С другой стороны, использование классического подхода требует в общем случае задания инвариантов циклов. Во-вторых, использование правил вывода для программных конструкций в их самом общем виде приводит к необходимости доказательства сложных формул в простых ситуациях. Нашим результатом, представленным в данной статье, является новая логика для решения данных проблем в случае циклов над последовательностями данных. Такая циклы мы называем финитными итерациями. Предложенную логику мы называем логикой для суждений о некорректности финитных итераций (IFIL). Мы избегаем задания инвариантов финитных итераций с помощью символической замены в условиях корректности переменных таких циклов применениями рекурсивных функций. Наша логика основана на специальных правилах вывода для финитных итераций. Эти правила позволяют выводить формулы с применениями рекурсивных функций, соответствующих финитным итерациям. Истинность этих формул может означать наличие ошибок в финитных итерациях. Данная логика была реализована в новой версии программной системы C-lightVer для дедуктивной верификации программ на языке C.

1. R. H"ahnle and M. Huisman, “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools,” in Computing and Software Science, vol. 10000, Springer, 2019, pp. 345–373.

2. K. R. Apt and E.-R. Olderog, “Fifty years of Hoare’s logic,” Formal Aspects of Computing, vol. 31, no. 6, pp. 751–807, 2019.

3. K. R. Apt and E.-R. Olderog, “Assessing the Success and Impact of Hoare’s Logic,” in Theories of Programming: The Life and Works of Tony Hoare, 2021, pp. 41–76.

4. C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol. 12, no. 10, pp. 576–580, 1969.

5. B. M"oller, P. O’Hearn, and T. Hoare, “On Algebra of Program Correctness and Incorrectness,” in Relational and Algebraic Methods in Computer Science, vol. 13027, Springer, 2021, pp. 325–343.

6. Q. L. Le, A. Raad, J. Villard, J. Berdine, D. Dreyer, and P. W. O’Hearn, “Finding Real Bugs in Big Programs with Incorrectness Logic,” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA1, pp. 1–27, 2022.

7. P. W. O’Hearn, “Incorrectness logic,” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 1–32, 2019.

8. A. Raad, J. Berdine, H.-H. Dang, D. Dreyer, P. O’Hearn, and J. Villard, “Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic,” in Computer Aided Verification, vol. 12225, Springer, 2020, pp. 225–252.

9. J. Vanegue, “Adversarial Logic,” in Static Analysis, vol. 13790, Springer, 2022, pp. 422–448.

10. M. Milanese and F. Ranzato, “Local Completeness Logic on Kleene Algebra with Tests,” in Static Analysis, vol. 13790, Springer, 2022, pp. 350–371.

11. B. Bruni, R. Giacobazzi, R. Gori, and F. Ranzato, “A Correctness and Incorrectness Program Logic,” Journal of the ACM, vol. 70, no. 2, pp. 1–45, 2023.

12. P. Maksimovi'c, C. Cronj"ager, A. L"o"ow, J. Sutherland, and P. Gardner, “Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding,” in 37th European Conference on Object-Oriented Programming (ECOOP 2023), vol. 263, Schloss Dagstuhl -- Leibniz-Zentrum f"ur Informatik, 2023, pp. 19:1–19:27.

13. N. Zilberstein, D. Dreyer, and A. Silva, “Outcome Logic: A Unifying Foundation of Correctness and Incorrectness Reasoning,” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 522–550, 2023.

14. T. Dardinier and P. M"uller, “Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version).” 2023.

15. A. Humenberger, M. Jaroschek, and L. Kov'acs, “Invariant Generation for Multi-Path Loops with Polynomial Assignments,” in Verification, Model Checking, and Abstract Interpretation, vol. 10747, Springer, 2018, pp. 226–246.

16. S. Chakraborty, A. Gupta, and D. Unadkat, “Full-program induction: verifying array programs sans loop invariants,” International Journal on Software Tools for Technology Transfer, vol. 24, no. 5, pp. 843–888, 2022.

17. V. A. Nepomniaschy, “Symbolic method of verification of definite iterations over altered data structures,” Programming and Computer Software, vol. 31, no. 1, pp. 1–9, 2005.

18. V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhailov, and A. V. Promskii, “Towards verification of C programs. C-light language and its formal semantics,” Programming and Computer Software, vol. 28, no. 6, pp. 314–323, 2002.

19. V. A. Nepomniaschy, I. S. Anureev, and A. V. Promskii, “Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language,” Programming and Computer Software, vol. 29, no. 6, pp. 338–350, 2003.

20. I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, and D. A. Kondratyev, “Automatic C Program Verification Based on Mixed Axiomatic Semantics,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 407–414, 2014.

21. D. A. Kondratyev and V. A. Nepomniaschy, “Automation of C Program Deductive Verification without Using Loop Invariants,” Programming and Computer Software, vol. 48, no. 5, pp. 331–346, 2022.

22. D. A. Kondratyev and A. V. Promsky, “The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs,” Automatic Control and Computer Sciences, vol. 54, no. 7, pp. 728–739, 2020.

23. J. S. Moore, “Milestones from the Pure Lisp Theorem Prover to ACL2,” Formal Aspects of Computing, vol. 31, no. 6, pp. 699–732, 2019.

24. D. A. Kondratyev, I. V. Maryasov, and V. A. Nepomniaschy, “The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination,” Automatic Control and Computer Sciences, vol. 53, no. 7, pp. 653–662, 2019.

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

26. S. Dailler, D. Hauzar, C. March'e, and Y. Moy, “Instrumenting a weakest precondition calculus for counterexample generation,” Journal of Logical and Algebraic Methods in Programming, vol. 99, pp. 97–113, 2018.

27. B. Becker, C. B. Lourencco, and C. March'e, “Explaining Counterexamples with Giant-Step Assertion Checking,” in Proceedings of the 6th Workshop on Formal Integrated Development Environment, vol. 338, 2021, pp. 82–88.

28. Q. L. Le, J. Sun, L. H. Pham, and S. Qin, “S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs.” 2022.

29. T. Dardinier, G. Parthasarathy, and P. M"uller, “Verification-Preserving Inlining in Automatic Separation Logic Verifiers,” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 789–818, 2023.

30. R. K"onighofer, R. Toegl, and R. Bloem, “Automatic Error Localization for Software Using Deductive Verification,” in Hardware and Software: Verification and Testing, vol. 8855, Springer, 2014, pp. 92–98.

31. P. Baudin et al., “The dogged pursuit of bug-free C programs: the Frama-C software analysis platform,” Communications of the ACM, vol. 64, no. 8, pp. 56–68, 2021.

32. M. R. Gadelha, F. Monteiro, L. Cordeiro, and D. Nicole, “ESBMC v6.0: Verifying C Programs Using $k$-Induction and Invariant Inference,” in Tools and Algorithms for the Construction and Analysis of Systems, vol. 11429, Springer, 2019, pp. 209–213.

33. S. L"owe, “CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation,” in Tools and Algorithms for the Construction and Analysis of Systems, vol. 7795, Springer, 2013, pp. 610–612.

34. D. Beyer and T. Lemberger, “CPA-SymExec: efficient symbolic execution in CPAchecker,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 900–903.

35. C. Cadar and M. Nowack, “KLEE symbolic execution engine in 2019,” International Journal on Software Tools for Technology Transfer, vol. 23, no. 6, pp. 867–870, 2021.

36. B. Jacobs, J. Kiniry, and M. Warnier, “Java Program Verification Challenges,” in Formal Methods for Components and Objects, vol. 2852, Springer, 2003, pp. 202–219.