ソフトウェア検証のための述語抽象化

ソフトウェア検証は重要で難しい問題です。多くのソフトウェアの静的チェック技術は、プログラマからのメソッド仕様やループ不変条件の形での注釈を必要とします。この注釈の負担、特にループ不変条件に関しては、静的チェックの採用における重要な障害です。私たちはループ不変条件を自動的に推論することで注釈の負担を軽減します。私たちの方法は、プログラム変数に対する与えられた述語の集合から抽象ドメインを構築する抽象解釈技術である述語抽象化に基づいています。私たちのアプローチの新しい特徴は、配列などの無限データを操作するプログラムを検証するために重要な普遍量化されたループ不変条件を推論することです。各ループに対して適切な述語を自動的に生成するためのヒューリスティックを提示します; プログラマは追加の述語を指定することもできます。また、一連の述語に関して状態の抽象を計算するための効率的なアルゴリズムを提示します。44KLOCのプログラムに対する実験では、私たちのアプローチが396のルーチンのうち31を除くすべてのルーチンに対して必要な述語と不変条件を自動的に推論できることを示しています。