C program verification in the multilanguage system spectrum

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.