ソフトウェアの検証に関する研究

Formative System Engineering
項書換え系を用いた多重文脈型定理証明の高速化
多重文脈型定理証明
 等式で表現された定理が、あるデータ構造上で成り立つかどうかの検証
 公理とデータ構造は項書換え系で表す
 項書換え系は等式に向きをつけた書換え規則の集合
研究目的
マルチコアを使い、項書換え系を用いた多重文脈型定理証明の効率を大きく上げる
等式
項書換え系
公理と
データ構造
停止性チェッカーは計算時間の
大部分を占める
多重文脈型定理
証明
停止性
チェッカー
仕様変更可能な
ツール
等式が成
り立つか
どうか
 基本のやり方は項書換え系の
ルールを各コアに割り当てて、
タスクを並列に実行する
 停止性検査のステップごとに違う設計
 順序関係などの潜在バグを排除
現在は様々な並列化手法を試しています

Download Report