Geodesic
Automatic C Program Verification Based on Mixed Axiomatic Semantics
Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 52-63.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: program verification, operational semantics, axiomatic semantics, C-light, partial correctness, LLVM, Simplify.
Mots-clés : C, C-kernel, ACSL 
@article{MAIS_2013_20_6_a3,
     author = {I. V. Maryasov and V. A. Nepomnyaschy and A. V. Promsky and D. A. Kondratyev},
     title = {Automatic {C} {Program} {Verification} {Based} on {Mixed} {Axiomatic} {Semantics}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {52--63},
     publisher = {mathdoc},
     volume = {20},
     number = {6},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a3/}
}
TY  - JOUR
AU  - I. V. Maryasov
AU  - V. A. Nepomnyaschy
AU  - A. V. Promsky
AU  - D. A. Kondratyev
TI  - Automatic C Program Verification Based on Mixed Axiomatic Semantics
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2013
SP  - 52
EP  - 63
VL  - 20
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a3/
LA  - ru
ID  - MAIS_2013_20_6_a3
ER  - 
%0 Journal Article
%A I. V. Maryasov
%A V. A. Nepomnyaschy
%A A. V. Promsky
%A D. A. Kondratyev
%T Automatic C Program Verification Based on Mixed Axiomatic Semantics
%J Modelirovanie i analiz informacionnyh sistem
%D 2013
%P 52-63
%V 20
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a3/
%G ru
%F MAIS_2013_20_6_a3
I. V. Maryasov; V. A. Nepomnyaschy; A. V. Promsky; D. A. Kondratyev. Automatic C Program Verification Based on Mixed Axiomatic Semantics. Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 52-63. http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a3/

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

[2] Kondratyev D. A., Promsky A. V., “Kompleksny podkhod k lokalizatsii oshibok pri verifikatsii Si-programm”, Sistemnaya informatika, 2013, no. 1, 79–96 (in Russian)

[3] Nepomnyaschy V. A., Anureev I. S., Mikhaylov I. N., Promsky A. V., “Orientirovanny na verifikatsiyu yazyk C-light”, Formalnye metody i modeli informatiki, sbornik nauchnykh trudov, Sistemnaya informatika, 9, Izdatelstvo SO RAN, Novosibirsk, 2004, 51–134 (in Russian)

[4] 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 | DOI

[5] I. Anureev, I. Maryasov, V. Nepomniaschy, “Revised Mixed Axiomatic Semantics Method of C Program Verification”, PSSV: Theory and Applications, Proc. of 3rd Workshop (Nizhni Novgorod, 2012), 16–23

[6] P. Baudin, P. Cuoq, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, V. Prevosto, ACSL: ANSI/ISO C Specification Language, http://frama-c.com/download/acsl_1.4.pdf

[7] T. Bormer, M. Brockschmidt, D. Distefano, G. Ernst, J.-C. Filliâtre, R. Grigore, M. Huisman, V. Klebanov, C. Marché, R. Monahan, W. Mostowski, N. Polikarpova, C. Scheben, G. Schellhorn, B. Tofan, J. Tschannen, M. Ulbrich, “The COST IC0701 Verification Competition 2011”, Revised Selected Papers of Int. Conf. FoVeOOS 2011, LNCS, 7421, 2011, 3–21

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

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

[10] J.-C. Filliâtre, C. Marché, “Multi-prover Verification of C Programs”, Proc. of 6th ICFEM, LNCS, 3308, 2004, 15–29

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

[12] K. R. M. Leino, “Dafny: An Automatic Program Verifier for Functional Correctness”, Revised Selected Papers of 16th Int. Conf. LPAR-16, LNCS, 6355, 2010, 348–370 | MR | Zbl

[13] I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, D. A. Kondratyev, “Automatic C Program Verification Based on Mixed Axiomatic Semantics”, Proc. of 4th Workshop “PSSV: Theory and Applications” (Yekaterinburg, 2013), 50–59

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

[15] 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 | DOI

[16] A. V. Promsky, A Formal Approach To The Error Localization, Preprint No 169, RAS. Sib. branch. IIS, Novosibirsk, 2012, 33 pp.