C program verification in SPECTRUM multilanguage system |
| |
| Authors: | V A Nepomniaschy I S Anureev M M Atuchin I V Maryasov A A Petrov A V Promsky |
| |
| Affiliation: | 1.A.P. Ershov Institute of Informatics Systems, Siberian Branch,Russian Academy of Sciences,Novosibirsk,Russia;2.Novosibirsk State University,Novosibirsk,Russia |
| |
| 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 application 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 programs 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 unified 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 verification of C programs based
on a combination of the operational, axiomatic, and transformational approaches. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
