Program verification system with synthesizer of invariant assertions

Seiichiro Dan, Takahira Yamaguchi, Osamu Kakusho, Yoshikazu Tezuka

研究成果: Article査読

1 被引用数 (Scopus)


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.

ジャーナルSystems and Computers in Japan
出版ステータスPublished - 1989

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • 情報システム
  • ハードウェアとアーキテクチャ
  • 計算理論と計算数学


「Program verification system with synthesizer of invariant assertions」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。