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

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

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