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


https://doi.org/10.18255/1818-1015-2017-6-743-754

Полный текст:


Аннотация

Данная работа представляет дальнейшее развитие метода верификации финитной итерации [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.


Дополнительные файлы

Для цитирования: Марьясов И.В., Непомнящий В.А., Кондратьев Д.А. Элиминация инвариантов финитных итераций над массивами при верификации Си программ. Моделирование и анализ информационных систем. 2017;24(6):743-745. https://doi.org/10.18255/1818-1015-2017-6-743-754

For citation: Maryasov I.V., Nepomniaschy V.A., Kondratyev D.A. Invariant Elimination of Definite Iterations over Arrays in C Programs Verification. Modeling and Analysis of Information Systems. 2017;24(6):743-745. https://doi.org/10.18255/1818-1015-2017-6-743-754

Просмотров: 220

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)