Program verification system with synthesizer of invariant assertions

Automatic verification system of programs is considered to be an important constituent in software development of the supporting environment. Detailed specifications including the invariant assertion of loops, are necessary for the program verification. Thus since it is very burdensome for humans to prepare them completely, the supporting environment is desired. Thus, we have been working on a theoretical investigation regarding the generation of invariant assertions, and furthermore, the construction of a program verification system with a synthesizer of invariant assertions. The theoretical investigation has already been reported, and this paper describes the implementation of our system and presents the results. Our system is a comprehensive program verification system which includes program input, obtaining specifications (invariant assertion generation), generating verification conditions, and proving the verification conditions. As synthesizers of invariant assertions, execution of difference equation method, tracing of program variables and path conditions by symbolic execution, and proposing invariant assertions by induction from trace information are realized. These functions are explained through executive examples and using computers, it is shown that the generation of invariant assertions and its support are possible. Also, since our system, including the proof system, is realized, it is more realistic and promising than existing program verification systems.