C Program Verication in the Multilanguage System Spectrum
Abstract
This paper presents the expendable multi-language analysis and verication system
SPECTRUM, which is being developed within the framework of the project SPEC-
TRUM. The project prospects are discussed using the example of C program verication.
The project aims at the development of a new integrated approach to program verica-
tion which will allow the integration, unication and combination of program verication
techniques together with accumulation and reuse of knowledge about them. One of the
project features consists in the use of the specialized executable specication language
Atoment. This language provides a unied format to represent both verication meth-
ods 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 verication
method. This method represents a good illustration of the integrated approach, since
it provides a complex C program verication that combines operational, axiomatic and
transformational approaches.
SPECTRUM, which is being developed within the framework of the project SPEC-
TRUM. The project prospects are discussed using the example of C program verication.
The project aims at the development of a new integrated approach to program verica-
tion which will allow the integration, unication and combination of program verication
techniques together with accumulation and reuse of knowledge about them. One of the
project features consists in the use of the specialized executable specication language
Atoment. This language provides a unied format to represent both verication meth-
ods 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 verication
method. This method represents a good illustration of the integrated approach, since
it provides a complex C program verication that combines operational, axiomatic and
transformational approaches.
Keywords
veri
cation,
speci
cation,
operational semantics,
axiomatic semantics,
domain-speci
c languages,
veri
cation systems
MSC2020: 519.681
About the Authors
V. A. Nepomniashy
Институт систем информатики имени А.П. Ершова СО РАН, Новосибирский государственный университет
Russian Federation
Russian Federation
I. S. Anureev
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
Russian Federation
M. M. Atuchin
Новосибирский государственный университет
Russian Federation
Russian Federation
I. V. Maryasov
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
Russian Federation
A. A. Petrov
Новосибирский государственный университет
Russian Federation
Russian Federation
A. V. Promsky
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
Russian Federation
References
1. Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C- программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28.
2. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. N 6. С. 1-16.
3. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: Сб. науч. тр. Новосибирск: Издательство СО РАН, 2004. Вып. 9: Формальные методы и модели информатики. С. 51-134.
4. Непомнящий В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20.
5. Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29.
6. Alkassar E., Hillebrand M.A., Leinenbach D., Schirmer N.W., Starostin A. The Verisoft Approach to Systems Verification // VSTTE 2008. Lect. Notes Comput. Sci. 2008. Vol. 5295. P. 209-224.
7. Cohen E., Dahlweid M., Hillebrand M.A., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. TPHOLs 2009. LNCS. 2009. Vol. 5674. P. 23-42.
8. Filliatre J.C., Marche C. Multi-prover verification of C programs // Proc. ICFEM 2004. LNCS. 2004. Vol. 3308. P. 15-29.
9. Jacobs B., Kiniry J.L., Warnier M. Java program verification challenges // Proc. FMCO 2002. Lect. Notes Comput. Sci. 2003. Vol. 2852. P. 202-219.
10. Promsky A.V. Towards C-light Program Verification: Overcoming the Obstacles // Proc. International Workshop on Program Understanding, 19-23 June, Altai Mountains, Russia, 2009. P. 53-63.
Review
For citations:
Nepomniashy V.A., Anureev I.S., Atuchin M.M., Maryasov I.V., Petrov A.A., Promsky A.V. C Program Verication in the Multilanguage System Spectrum. Modeling and Analysis of Information Systems. 2010;17(4):88-100. (In Russ.)
Views:
534
Email this article 