Tarasich Y. The static analysis of linearly defined programs and its application

The main aim of the work is to analyze the existing algorithms of computer algebra and insertion modeling in the systems of software static analysis and verification and to build an effective algorithms for static analysis of programs. In Section 1 an analysis of existing methods and systems of static analysis and basic definitions of dissertation research are provided. In Section 2 the problem of invariants generation was considered, the new method for proving the invariance of the system of linear inequalities, and also the completion of linearly defined iterative cycles of imperative programs were presented. In Section 3 a new algorithm for constructing the canonical form of linear semi-algebraic (LSF) formulas and its realization are presented. The practical significance of the expected scientific results lies in the possibility of applying scientific provisions and research conclusions in software verification tasks, namely in the development of specialized software systems for verification of formal program models.