C Program Verification in SPECTRUM Multilanguage
System

V. A. Nepomniaschy, I. S. Anureev, M. M. Atuchin, I. V. Maryasov,
A. A. Petrov, and A. V. Promsky

A.P. Ershov Institute of Informatics Systems, Siberian Branch, Russian Academy of Sciences, pr. Lavrent’eva 6,
Novosibirsk, 630090 Russia

Novosibirsk State University, ul. Pirogova 2, Novosibirsk, 630090 Russia

e-mail: vnep@iis.nsk.su; anureev@iis.nsk.su; promsky@iis.nsk.su

Received October 18, 2010

Abstract—An extendable multilanguage analysis and verification system SPECTRUM is presented;
this system is being developed in the framework of the project SPECTRUM. The prospects of the appli-
cation of this system are demonstrated, as exemplified by the verification of C programs. The project
SPECTRUM is aimed at the creation of a new integrated approach to the verification of imperative pro-
grams that makes it possible to integrate, unify, and combine methods and approaches for verification of
imperative programs and accumulate and apply information about these programs. The specific feature
of this approach is the application of a specialized executable specification language Atoment for the
development of program verification tools; this language makes it possible to represent methods and
approaches for verification and data for them (program models, annotations, logical formulae) in a uni-
fied format. The C component of the SPECTRUM system uses a two-level C program verification
method. This method is a good illustration of the integrated approach, since it provides complex verifi-
cation of C programs based on a combination of the operational, axiomatic, and transformational
approaches.

Keywords: verification, specification, operational semantics, axiomatic semantics, domain-specific lan-
guages, verification systems

DOI: 10.3103/S014641161107011X

Pleiades Publishing home page | journal home page | top

If you have any problems with this server, contact webmaster.