Автоматическая верификация C-программ на основе смешанной аксиоматической семантики


https://doi.org/10.18255/1818-1015-2013-6-52-63

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


Аннотация

Развитие проекта C-light привело к применению новых формализмов и реализации методов, которые облегчают процесс верификации С-программ. Смешанная аксиоматическая семантика предлагает выбор между упрощенными и общими правилами вывода условий корректности (УК) в зависимости от программных объектов и их свойств. Инфраструктура LLVM значительно упрощает реализацию анализатора и транслятора C-light программ. Метод семантических меток, предложенный ранее, теперь может быть безопасно исполь- зован в условиях корректности при их доказательстве. Рассмотрен пример из соревнования по верификации, иллюстрирующий применение нашей системы.


Об авторах

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

младший научный сотрудник,

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



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

зав. лабораторией,

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

доцент,

630090, г. Новосибирск, ул. Пирогова, д. 2



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

научный сотрудник,

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



Дмитрий Александрович Кондратьев
Новосибирский государственный университет
Россия

студент,

630090, г. Новосибирск, ул. Пирогова, д. 2



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

1. Gamma E., Helm R., Johnson R., Vlissides J. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994. 395 p.

2. Кондратьев Д. А., Промский А. В. Комплексный подход к локализации ошибок при верификации Си-программ // Системная информатика. 2013. № 1. С. 79–96 (Kondratyev D.A., Promsky A.V. Kompleksny podkhod k lokalizatsii oshibok pri verifikatsii Si-programm // Sistemnaya informatika. 2013. N 1. P. 79–96 [in Russian]).

3. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: сборник научных трудов. Новосибирск: Издательство СО РАН. 2004. Вып. 9: Формальные методы и модели информатики. С. 51 – 134 (Nepomnyaschy V.A., Anureev I.S., Mikhaylov I.N., Promsky A.V. Orientirovanny na verifikatsiyu yazyk C-light // Sistemnaya informatika: sbornik nauchnykh trudov. Novosibirsk: Izdatelstvo SO RAN, 2004. Vyp. 9: Formalnye metody i modeli informatiki. P. 51 – 134 [in Russian]).

4. Anureev I.S., Maryasov I.V., Nepomniaschy V.A. C-programs Verification Based on Mixed Axiomatic Semantics // Automatic Control and Computer Sciences. 2011. Vol. 45. Issue 7. P. 485–500.

5. Anureev I., Maryasov I., Nepomniaschy V. Revised Mixed Axiomatic Semantics Method of C Program Verification // Proc. of 3rd Workshop "PSSV: Theory and Applications". Nizhni Novgorod, 2012. P. 16–23.

6. Baudin P., Cuoq P., Filliˆatre J.-C., March´e C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. http://frama-c.com/download/acsl_1.4.pdf

7. Bormer T., Brockschmidt M., Distefano D., Ernst G., Filliˆatre J.-C., Grigore R., Huisman M., Klebanov V., March´e C., Monahan R., Mostowski W., Polikarpova N., Scheben C., Schellhorn G., Tofan B., Tschannen J., Ulbrich M. The COST IC0701 Verification Competition 2011 // Revised Selected Papers of Int. Conf. FoVeOOS 2011. LNCS. 2011. Vol.7421. P. 3–21.

8. Cohen E., Dahlweid M., Hillebrand M., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. of 22nd Int. Conf. TPHOLs. LNCS. 2009. Vol. 5674. P. 23–42.

9. Detlefs D., Nelson G., Saxe J. B. Simplify: A Theorem Prover for Program Checking. Palo Alto, 2003. 121 p. (HP Tech. Rep. HPL-2003-148). http://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdf

10. Filliˆatre J.-C., March´e C. Multi-prover Verification of C Programs // Proc. of 6th ICFEM. LNCS. 2004. Vol. 3308. P. 15–29.

11. Klebanov V., M¨uller P., Shankar N., Leavens G. T., W¨ustholz V., Alkassar E., Arthan R., Bronish D., Chapman R., Cohen E., Hillebrand M., Jacobs B., Leino K. R. M., Monahan R., Piessens F., Polikarpova N., Ridge T., Smans J., Tobies S., Tuerk T., Ulbrich M., Weiß B. The 1st Verified Software Competition: Experience Report // Proc. 17th Int. Symp. on Formal Methods. LNCS. 2011. Vol. 6664. P. 154–168.

12. Leino K.R.M. Dafny: An Automatic Program Verifier for Functional Correctness // Revised Selected Papers of 16th Int. Conf. LPAR-16. LNCS. 2010. Vol. 6355. P. 348–370.

13. Maryasov I.V., Nepomniaschy V.A., Promsky A.V., Kondratyev D.A. Automatic C Program Verification Based on Mixed Axiomatic Semantics // Proc. of 4th Workshop "PSSV: Theory and Applications". Yekaterinburg, 2013. P. 50–59.

14. Moura L. de, Bjørner N. Z3: An Efficient SMT Solver // Proc. of 14th Int. Conf. TACAS 2008. LNCS. 2008. Vol. 4963. P. 337–340.

15. Nepomniaschy V.A., Anureev I.S., Atuchin M.M., Maryasov I.V., Petrov A.A., Promsky A.V. C Program Verification in SPECTRUM Multilanguage System // Automatic Control and Computer Sciences. 2011. Vol. 45. Issue 7. P. 413–420.

16. Promsky A.V. A Formal Approach To The Error Localization. Novosibirsk, 2012. 33 p. (Preprint / RAS. Sib. branch. IIS; No 169).


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

Для цитирования: Марьясов И.В., Непомнящий В.А., Промский А.В., Кондратьев Д.А. Автоматическая верификация C-программ на основе смешанной аксиоматической семантики. Моделирование и анализ информационных систем. 2013;20(6):52-63. https://doi.org/10.18255/1818-1015-2013-6-52-63

For citation: Maryasov I.V., Nepomnyaschy V.A., Promsky A.V., Kondratyev D.A. Automatic C Program Verification Based on Mixed Axiomatic Semantics. Modeling and Analysis of Information Systems. 2013;20(6):52-63. (In Russ.) https://doi.org/10.18255/1818-1015-2013-6-52-63

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

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

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


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


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