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/