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/