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

摘要

プログラム検証において，ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている．しかし，検証に有効なループ不変式を自動的に発見することは一般には困難である．本稿では，プログラム変数と関数呼び出し項に関する非線形の不等式で表されるループ不変式を，線形計画法などで利用されるFarkasの補題を拡張した定理に基づいて自動生成する手法を示す．