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


https://doi.org/10.18255/1818-1015-2015-6-773-782

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


Аннотация

Верификация С-программ является актуальной проблемой современного программирования. Для применения известных методов дедуктивной верификации необходимо аннотировать циклы посредством инвариантов, что во многих случаях является трудной задачей. В этой статье мы рассматриваем язык C-light, который является выразительным подмножеством языка C, соответствующего стандарту ISO. Для верификации C-light программ нами были предложены двухуровневый подход [19, 20] и метод смешанной аксиоматической семантики [1, 3, 11]. На первой стадии этого подхода исходная C-light программа транслируется [17] в программу на языке C-kernel [19], который является подмножеством языка C-light. Теорема о корректности этой трансляции была доказана в [10, 11]. По сравнению с C-light в языке C-kernel меньше операторов, что позволяет уменьшить число правил вывода при разработке аксиоматической семантики. На второй стадии этого подхода для программ на языке C-kernel порождаются условия корректности по правилам смешанной аксиоматической семантики [10, 11], которая может содержать несколько правил вывода для одной и той же программной конструкции. В таких случаях правила вывода применяются однозначно в зависимости от контекста. Заметим, что во многих случаях использование смешанной аксиоматической семантики позволяет упростить условия корректности. В этой статье представлено расширение данного подхода, которое включает наш метод верификации для финитной итерации над неизменяемыми структурами данных без выхода из тела цикла в C-light программах. Данный метод содержит новое правило вывода для таких финитных итераций без инвариантов. Это правило было реализовано в генераторе условий корректности. На стадии доказательства используется SMT-решатель Z3 [12]. Рассмотрен пример, иллюстрирующий применение данного подхода.

Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.

Статья публикуется в авторской редакции.


Об авторах

И. В. Марьясов
Институт систем информатики им. А.П. Ершова СО РАН
Россия

канд. физ.-мат. наук,

пр. Академика Лаврентьева, 6, г. Новосибирск, 630090



В. А. Непомнящий
Институт систем информатики им. А.П. Ершова СО РА
Россия

канд. физ.-мат. наук, доцент,

пр. Академика Лаврентьева, 6, г. Новосибирск, 630090



Список литературы

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, http://link.springer.com/article/10.3103/S0146411611070029.

2. I. Anureev, I. Maryasov, V. Nepomniaschy, “Revised Mixed Axiomatic Semantics Method of C Program Verification”, Proceedings, Third Workshop ”Program Semantics, Specification and Verification: Theory and Applications”, PSSV 2012 (Nizhni Novgorod, Russia, July 1–2), eds. Valery Nepomniaschy, Valery Sokolov, 2012, 16–23.

3. I. S. Anureev, I. V. Maryasov, V. A. Nepomniaschy, “Two-level Mixed Verification Method of C-light Programs in Terms of Safety Logic”, Computer Science, 34, NCC Publisher, 2012, 23–42.

4. M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, K. Rustan M. Leino, “Boogie: A Modular Reusable Verifier for Object-Oriented Programs”, Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005 (Amsterdam, The Netherlands, November 1-4), Lecture Notes in Computer Science, 4111, Springer, 2006, 364–387, http://link.springer.com/chapter/10.1007/11804192 17.

5. E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, S. Tobies, “VCC: A Practical System for Verifying Concurrent C”, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009 (Munich, Germany, August 17–20), Lecture Notes in Computer Science, 5674, Springer, 2009, 23–42, http://link.springer.com/chapter/10.1007/978-3-642-03359-9 2.

6. J.-C. Filliˆatre, C. March´e, “Multi-prover Verification of C Programs”, Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004 (Seattle, WA, USA, November 8–12), Lecture Notes in Computer Science, 3308, Springer, 2004, 15–29, http://link.springer.com/chapter/10.1007/978-3-540-30482-1 10.

7. K. Rustan M. Leino, “Automating Induction with an SMT Solver”, Verification, Model Checking, and Abstract Interpretation, 13th International Conference, VMCAI 2012 (Philadelphia, PA, USA, January 22–24), Lecture Notes in Computer Science, 7148, Springer, 2012, 315–331, http://link.springer.com/chapter/10.1007/978-3-642-27940-9 21.

8. K. Rustan M. Leino, “Dafny: An Automatic Program Verifier for Functional Correctness”, Logic for Programming, Artificial Intelligence, and Reasoning, 16th International Conference, LPAR-16 (Dakar, Senegal, April 25–May 1), Lecture Notes in Computer Science, 6355, Springer, 2010, 348–370, http://link.springer.com/chapter/10.1007/978-3-642-17511-4 20.

9. X. Leroy, “Formal Verification of a Realistic Compiler”, Communications of the ACM, 52:7 (2009), 107–115.

10. I. V. Maryasov, The Mixed Axiomatic Semantics Method, Novosibirsk, Siberian Division of the Russian Academy of Sciences, A. P. Ershov Institute of Informatics Systems, 160, 2011, http://www.iis.nsk.su/files/preprints/160.pdf.

11. 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, http://link.springer.com/article/10.3103/S0146411614070141.

12. L. de Moura, N. Bjørner, “Z3: An Efficient SMT Solver”, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008 (Budapest, Hungary, March 29–April 6), Lecture Notes in Computer Science, 4963, Springer, 2008, 337–340, http://link.springer.com/chapter/10.1007/978-3-540-78800-3 24.

13. V. A. Nepomniaschy, “Symbolic Verification Method for Definite Iteration over Altered Data Structures”, Programming and Computer Software, 1 (2005), 1–12.

14. V. A. Nepomniaschy, “Verification of Definite Iteration over Hierarchical Data structures”, Fundamental Approaches to Software Engineering, Second International Conference, FASE’99 (Amsterdam, The Netherlands, March 22–28), Lecture Notes in Computer Science, 1577, Springer, 1999, 176–187, рttp://link.springer.com/chapter/10.1007/978-3-540-49020-3 12.

15. V. A. Nepomniaschy, “Verification of Definite Iteration over Tuples of Data Structures”, Programming and Computer Software, 1 (2002), 1–10.

16. V. A. Nepomniaschy, I. S. Anureev, M. M. Atuchin, I. V. Maryasov, A. A. Petrov, A. V. Promsky, “C Program Verification in SPECTRUM Multilanguage System”, Automatic Control and Computer Sciences, 45:7 (2011), 413–420, http://link.springer.com/article/10.3103/S014641161107011X.

17. V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhaylov, A. V. Promsky, Towards The Verification of C Programs. Part 3. Translation From C-light To C-light-kernel and Its Formal Proof, Novosibirsk, Siberian Division of the Russian Academy of Sciences, A. P. Ershov Institute of Informatics Systems, 97, 2002 (Russian), http://www.iis.nsk.su/files/preprints/097.pdf.

18. V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Towards Verification of C Programs. C-light Language and Its Formal Semantics”, Programming and Computer Software, 28 (2002), 314–323.

19. V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Towards Verification of C Programs. Axiomatic Semantics of The C-kernel Language”, Programming and Computer Software, 29 (2003), 338–350.

20. V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Verification-Oriented Language CLight and Its Structural Operational Semantics”, Perspectives of System Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003 (Akademgorodok, Novosibirsk, Russia, July 9–12), Lecture Notes in Computer Science, 2890, Springer, 2003, 103–111, http://link.springer.com/chapter/10.1007/978-3-540-39866-0 12.


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

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

For citation: Maryasov I.V., Nepomniaschy V.A. Loop Invariants Elimination for Definite Iterations over Unchangeable Data Structures in C Programs. Modeling and Analysis of Information Systems. 2015;22(6):773-782. (In Russ.) https://doi.org/10.18255/1818-1015-2015-6-773-782

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

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

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


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


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