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/

[1] 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

[2] V. A. Nepomnyaschii, I. S. Anureev, I. N. Mikhailov, A. V. Promskii, “Na puti k verifikatsii S programm. Aksiomaticheskaya semantika yazyka C-kernel”, Programmirovanie, 2003, no. 6, 1–16

[3] V. A. Nepomnyaschii, I. S. Anureev, I. N. Mikhailov, A. V. Promskii, “Orientirovannyi na verifikatsiyu yazyk C-light”, Formalnye metody i modeli informatiki, Sb. nauch. tr., Sistemnaya informatika, 9, Izdatelstvo SO RAN, Novosibirsk, 2004, 51–134

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

[5] I. S. Anureev, “A three-stage method of C program verification”, Joint NCC Bulletin, Computer Science, 28, 2008, 1–29

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

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

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

[9] B. Jacobs, J. L. Kiniry, M. Warnier, “Java program verification challenges”, Proc. FMCO 2002, Lect. Notes Comput. Sci., 2852, 2003, 202—219 | Zbl

[10] A. V. Promsky, “Towards C-light Program Verification: Overcoming the Obstacles”, Proc. International Workshop on Program Understanding (19–-23 June, Altai Mountains, Russia), 2009, 53–63