Geodesic
C program verification in the multilanguage system spectrum
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 88-100

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

This paper presents the expendable multi-language analysis and verification system SPECTRUM, which is being developed within the framework of the project SPECTRUM. The project prospects are discussed using the example of C program verification. The project aims at the development of a new integrated approach to program verification which will allow the integration, unification and combination of program verification techniques together with accumulation and reuse of knowledge about them. One of the project features consists in the use of the specialized executable specification language Atoment. This language provides a unified format to represent both verification methods and data for them (program models, annotations, logic formulas). The C-targeted component of the SPECTRUM system is based on our two-level C program verification method. This method represents a good illustration of the integrated approach, since it provides a complex C program verification that combines operational, axiomatic and transformational approaches.
Keywords: verification, specification, operational semantics, axiomatic semantics, domain-specific languages, verification systems. 
@article{MAIS_2010_17_4_a9,
     author = {V. A. Nepomnyashchii and I. S. Anureev and M. M. Atuchin and I. V. Mar'yasov and A. A. Petrov and A. V. Promskii},
     title = {C program verification in the multilanguage system spectrum},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {88--100},
     publisher = {mathdoc},
     volume = {17},
     number = {4},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a9/}
}
TY  - JOUR
AU  - V. A. Nepomnyashchii
AU  - I. S. Anureev
AU  - M. M. Atuchin
AU  - I. V. Mar'yasov
AU  - A. A. Petrov
AU  - A. V. Promskii
TI  - C program verification in the multilanguage system spectrum
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 88
EP  - 100
VL  - 17
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a9/
LA  - ru
ID  - MAIS_2010_17_4_a9
ER  - 
%0 Journal Article
%A V. A. Nepomnyashchii
%A I. S. Anureev
%A M. M. Atuchin
%A I. V. Mar'yasov
%A A. A. Petrov
%A A. V. Promskii
%T C program verification in the multilanguage system spectrum
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 88-100
%V 17
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a9/
%G ru
%F MAIS_2010_17_4_a9
V. A. Nepomnyashchii; I. S. Anureev; M. M. Atuchin; I. V. Mar'yasov; A. A. Petrov; A. V. Promskii. C program verification in the multilanguage system spectrum. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 88-100. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a9/