Integrated approach to analysis and verification of imperative programs

This paper describes a new approach to the analysis and verification of imperative programs, which allows us to integrate, unify and combine the methods and techniques of analysis and verification of imperative programs, accumulate and use knowledge about them. A feature of the approach is to use the domain-specific language Atoment, designed to develop tools for analysis and verification of programs, which allows us to represent both methods and techniques of analysis and verification and data for them (program models, annotations, inference rules, etc.) in a single unified format. The paper includes an introduction to the language Atoment, a description of a multilanguage system Spectrum of analysis and verification of programs, based on this language, and a methodology of applying this approach to verification of imperative programs by example of the C-light language.