Geodesic
Attribute annotations and their use in C program deductive verification
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 21-33.

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

In this paper a new kind of annotations, called attribute annotations, and the methodology for their application in a deductive program verification are proposed. A collection of annotating attributes for the subset C-kernel of the C language is described, and on their base two versions of axiomatic semantics of C-kernel – forward semantics and mixed forward semantics – are presented.
Keywords: deductive verification, attribute normalization, axiomatic semantics, C-light
Mots-clés : attribute annotations, C-kernel. 
@article{MAIS_2011_18_4_a2,
     author = {M. M. Atuchin and I. S. Anureev},
     title = {Attribute annotations and their use in {C} program deductive verification},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {21--33},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a2/}
}
TY  - JOUR
AU  - M. M. Atuchin
AU  - I. S. Anureev
TI  - Attribute annotations and their use in C program deductive verification
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 21
EP  - 33
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a2/
LA  - ru
ID  - MAIS_2011_18_4_a2
ER  - 
%0 Journal Article
%A M. M. Atuchin
%A I. S. Anureev
%T Attribute annotations and their use in C program deductive verification
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 21-33
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a2/
%G ru
%F MAIS_2011_18_4_a2
M. M. Atuchin; I. S. Anureev. Attribute annotations and their use in C program deductive verification. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 21-33. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a2/

[1] X. Leroy, “Formal verification of a realistic compiler”, Communications of the ACM, 52(7) (2009), 107–115 | DOI

[2] J. C. Filliâtre, C. Marché, “Multi-prover verification of C programs”, Proc. ICFEM 2004, LNCS, 3308, 2004, 15–29

[3] K. R. M. Leino, P. Rümmer, “A polymorphic intermediate verification language: Design and logical encoding”, TACAS 2010, LNCS, 6015, 2010, 312–327 | Zbl

[4] K. R. M. Leino, “Dafny: an automatic program verifier for functional correctness”, LPAR-16, LNCS, 6355, 2010, 348–370 | Zbl

[5] E. Cohen, M. Dahlweid, M. Hillebrand, et al., “VCC: A Practical System for Veirying Concurrent C”, TPHOLs 2009, LNCS, 5674, 2009, 23–42 | MR | Zbl

[6] E. Alkassar, M. A. Hillebrand, D. Leinenbach, N. W. Schirmer, A. Starostin, “The Verisoft Approach to Systems Verification”, VSTTE 2008, LNCS, 5295, 2008, 209–224

[7] V. A. Nepomnyaschii, I. S. Anureev, A. V. Promskii, “Na puti k verifikatsii S programm. Aksiomaticheskaya semantika yazyka C-kernel”, Programmirovanie, 2003, no. 6, 5–15

[8] V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Verification-oriented language C-light and its structural operational semantics”, Proc. of Conf. PSI-2003, LNCS, 2890, 2003, 1–5

[9] V. A. Nepomnyaschii, I. S. Anureev, I. N. Mikhailov, A. V. Promskii, “Na puti k verifikatsii S programm. Yazyk C-light i ego formalnaya semantika”, Programmirovanie, 2002, no. 6, 1–13

[10] V. A. Nepomnyaschii, I. S. Anureev, A. V. Promskii, “Na puti k verifikatsii C-programm. Yazyk S-light i ego transformatsionnaya semantika”, Problemy programmirovaniya, 2006, no. 2, 359–368

[11] V. A. Nepomnyaschii, I. S. Anureev, I. N. Mikhailov, A. V.Promskii, “Orientirovannyi na verifikatsiyu yazyk C-light”, Formalnye metody i modeli informatiki, Sbornik nauchnykh trudov, Seriya «Sistemnaya informatika», Izdatelstvo SO RAN, Novosibirsk, 2004, 51–134

[12] I. S. Anureev, I. V. Maryasov, V. A. Nepomnyaschii, “Verifikatsiya C-programm na osnove smeshannoi aksiomaticheskoi semantiki”, Modelirovanie i analiz informatsionnykh sistem, 17:3 (2010), 5–28

[13] ISO/IEC 9899: Programming languages – C, 1999

[14] V. A. Nepomniaschy, A. A. Sulimov, “Promlem-oriented means of program specification and verification in project SPECTRUM”, DISCo 1993, LNCS, 722, 1993, 374–378

[15] V. A. Nepomniaschy, A. A. Sulimov, “Problem-oriented verification system and its application to linear algebra programs”, Theoretical Computer Science, 119 (1993), 173–185 | DOI | MR | Zbl

[16] V. A. Nepomnyaschii, I. S. Anureev, A. V. Promskii, I. V. Dubranovskii, “Na puti k verifikatsii C# programm: trekhurovnevyi podkhod”, Programmirovanie, 2006, no. 4, 4–20

[17] I. S. Anureev, “Introduction to the Atoment language”, Joint NCC Bulletin, Series Computer Science, 30, 2010, 1–16

[18] V. A. Nepomnyaschii, I. S. Anureev, M. M. Atuchin, I. V. Maryasov, A. A. Petrov, A. V. Promskii, “Sistema analiza i verifikatsii C-programm SPEKTR-2”, Modelirovanie i analiz informatsionnykh sistem, 17:4 (2010), 88–100