Automatic C Program Verification Based on Mixed Axiomatic Semantics
https://doi.org/10.18255/1818-1015-2013-6-52-63
Abstract
The development of the C-light project resulted in the application of new formalisms and implementation techniques which facilitate the verification process. The mixed axiomatic semantics proposes a choice between simplified and full-strength deduction rules depending on program objects and their properties. The LLVM infrastructure helps greatly in writing the C-light program analyzer and translator. The semantical labeling technique, proposed earlier, can now be safely kept in verification conditions during their proof. Two programs from the well-known verification benchmarks illustrate the applicability of the system.
About the Authors
I. V. Maryasov
A.P. Ershov Institute of Informatics Systems SB RAS
Russian Federation
Russian Federation
младший научный сотрудник,
prospect Akademika Lavrentjeva, 6, Novosibirsk, 630090, Russia
V. A. Nepomnyaschy
A.P. Ershov Institute of Informatics Systems SB RAS;
Novosibirsk State University
Russian Federation
Russian Federation
зав. лабораторией,
prospect Akademika Lavrentjeva, 6, Novosibirsk, 630090, Russia;
доцент,
Pirogova Str., 2, Novosibirsk, 630090, Russia
A. V. Promsky
A.P. Ershov Institute of Informatics Systems SB RAS
Russian Federation
Russian Federation
научный сотрудник,
prospect Akademika Lavrentjeva, 6, Novosibirsk, 630090, Russia
D. A. Kondratyev
Novosibirsk State University
Russian Federation
Russian Federation
студент,
Pirogova Str., 2, Novosibirsk, 630090, Russia
References
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).
Review
For citations:
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
Views:
1443
Email this article 