関数呼び出しを持つプログラムの非線形ループ不変式の自動生成

摘要

Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automatically find meaningful loop invariants. In this report, we present a method for automatically generating loop invariants in the form of extended polynomial inequality, in which function instances may be in­cluded, over program variables. The method is based on the extended polynomial lemma which is improved to Farkas' Lemma.%プログラム検証において，ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている.しかし，検証に有効なループ不変式を自動的に発見することは一般には困難である.本稿では，プログラム変数と関数呼び出し項に関する非線形の不等式で表されるループ不変式を，線形計画法などで利用されるFarkasの補題を拡張した定理に基づいて自動生成する手法を示す.