Элиминация инвариантов финитных итераций над массивами при верификации Си программ

Данная работа представляет дальнейшее развитие метода верификации финитной итерации [7]. Он расширяет метод смешанной аксиоматической семантики [1], предложенный для верификации C-light программ. Это расширение включает метод верификации для финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Данное правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности применяется метод математической индукции, вызывающий сложности у SMT-решателей. В нашей системе верификации на стадии доказательства используется SMT-решатель CVC4. Для преодоления упомянутой трудности применяется стратегия переписывания условий корректности. Для доказательства условий корректности предложен метод, основанный на расширении теории новыми теоремами. Рассмотрен пример, иллюстрирующий применение данных методов. Статья публикуется в авторской редакции.

1. I. S. Anureev, I. V. Maryasov, V. A. Nepomniaschy, “C-programs Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 45:7 (2011), 485–500.

2. C. Barrett, C. L., Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, C. Tinelli, “CVC4”, 23rd Int. Conf. CAV, Lecture Notes in Computer Science, 6806 (2011), 171–177.

3. E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte,S. Tobies, “VCC: A Practical System for Verifying Concurrent C”, 22nd Int. Conf.TPHOLs, Lecture Notes in Computer Science, 5674 (2009), 23–42.

4. J.-C. Filli˄atre, C. March´e, “Multi-prover Verification of C Programs”, 6th ICFEM, Lecture Notes in Computer Science, 3308 (2004), 15–29.

5. D. A. Kondratyev, “The Extension of the MetaVCG Approach by Semantic Mark-up Concept”, Int. Workshop-conf. ”Tools & Methods of Program Analysis”, St. Petersburg, 2015, 107–118.

6. K. R. M. Leino, “Automating Induction with an SMT Solver”, 13th Int. Conf. VMCAI, Lecture Notes in Computer Science, 7148 (2012), 315–331.

7. I. V. Maryasov, V. A. Nepomniaschy, “Loop Invariants Elimination for Definite Iterations over Unchangeable Data Structures in C Programs”, Modeling and Analysis of Information Systems, 22:6 (2015), 773–782.

8. I. V. Maryasov, V. A. Nepomniaschy, D. A. Kondratyev, “Verification of Definite Iteration over Arrays with a Loop Exit in C Programs”, System Informatics, 2017, š 10, 57–66.

9. 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.

10. M. Moriconi, R. L. Schwarts, “Automatic Construction of Verification Condition Generators From Hoare Logics”, Automata, Languages and Programming, Lecture Notes in Computer Science, 115 (1981), 363–377.

11. V. A. Nepomniaschy, “Verification of Definite Iteration over Hierarchical Data Structures”, FASE/ ETAPS, Lecture Notes in Computer Science, 1577 (1999), 176–187.

12. A. Reynolds, V. Kuncak, “Induction for SMT solvers”, 16th Int. Conf. VMCAI, Lecture Notes in Computer Science, 8931 (2015), 80–98.

13. T. Tuerk, “Local Reasoning about While-Loops”, VSTTE, 2010, 29–39.