| Outline of Annual Research Achievements |
本研究の目的は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系を定義し, その論理体系に対して, 定理証明, 両仮説形成, 記号計算のループインバリアント生成の三つを計算する効率よいアルゴリズムを与え, それらのアルゴリズムの正しさおよび決定可能性を数学的に証明し, またそれらのアルゴリズムの効率を実装実験により証拠付けることである. 本研究では, 次のような研究を行った. 一般的帰納的述語に対して循環証明を, 配列および算術に対してプレスバーガー算術への翻訳を, ループインバリアント生成アルゴリズムに対してゲージ領域などの既知の最新の抽象領域の組み合わせを, それぞれアイデアとして研究を進めた. 記号実行のループインバリアント生成は記号区間領域, ゲージ領域などの既知の最新の抽象領域を組み合わせ, これを拡張された分離論理に適用することによりよいアルゴリズムを構成する研究を行った. 有界木幅帰納的述語のある記号ヒープのエンテイルメントの真偽を, 循環証明体系により計算する判定器を構成し, その決定可能性定理を証明する研究を行った. 決定可能性の証明のアイデアとして, 有限個の標準形により証明探索空間が限定できること, unfold match を分離含意により拡張することを用いて研究を行った. 配列と算術をもつ分離論理に関して, 既存研究を発展させて, 配列, 算術, リスト述語を同時にもつ分離論理に対するアルゴリズムを構成しその決定可能性を証明する研究を行った. 配列とリストはその性質によりヒープ中で分離できること, プレスバーガー算術への翻訳をアイデアとして研究を進めた. この実装システムを用いてOpenSSLのCコードのメモリー安全性を検証しつつある. 理論, 実装, 実験を互いにフィードバックさせながら研究を進めており完成に近づいている.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
分離論理を一般帰納的述語により拡張する研究と, 分離論理を配列と算術により拡張する研究を並行に行った. それぞれの拡張では, まず, 拡張した論理体系を定義し, 次に, その論理体系に対して, 定理証明, 両仮説形成, 記号計算のループインバリアント生成の三つを計算する効率よいアルゴリズムを与え, それらのアルゴリズムの正しさおよび決定可能性を数学的に証明し, またそれらのアルゴリズムの効率を実装実験により証拠付ける研究を行った. 定理証明としては記号ヒープのエンテイルメントの判定を研究した. 本研究では, 両仮説形成を用いて, 記号実行においてモジュラー性を次のように可能にする研究を行った. まず部分手続きの事前事後条件を計算し, 次にその部分手続きがよばれる場所にこの事前事後条件を適用するときに, 両仮説形成がその適用方法を計算する. 本研究では, 得られたエンテイルメント判定アルゴリズムを変形することにより両仮説形成アルゴリズムを得る研究を行った. 以上により進捗はおおむね良好であるといえる.
|
| Strategy for Future Research Activity |
一般帰納的定義を扱うシステムだけではなく, 一般帰納的定義のうちで実際のソフトウェア検証によく現れるリストを特別に高速に扱えるシステムの研究も行う. リストに関する効率のよいシステムが完成したら, それを一般的帰納的定義のシステムに組み込み, 一般的帰納的定義はすべて扱えるが, リストは特に高速に扱えるシステムを完成させる研究を行う. さらに, 分離論理を一般帰納的述語, 配列, 算術により同時に拡張する研究を行う. まず, 同時に拡張した論理体系を定義し, 次に, その論理体系に対して, 定理証明, 両仮説形成, 記号計算のループインバリアント生成の三つを計算する効率よいアルゴリズムを与え, それらのアルゴリズムの正しさおよび決定可能性を数学的に証明し, またそれらのアルゴリズムの効率を実装実験により証拠付ける.
|
