2018 Fiscal Year Research-status Report
Development of Verification Techniques for Equivalence of Programs via Rewriting Induction
| Project/Area Number |
18K11160
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | プログラム検証 / 項書換えシステム / プログラム変換 / 計算モデル / 帰納法 / 定理自動証明 / 補題生成 |
|---|
| Outline of Annual Research Achievements |
初年度はまずC言語で書かれたプログラムを対象に，ポインタ以外の基本データ型やユーザ定義データ型（構造体や共用体を含む）を扱うプログラムを固定長の0,1の列であるビットベクトル上で定義された論理制約付き項書換えシステムに変換する枠組みを構築し，実装した．その際に，大域変数とそれにアクセスする関数を扱うプログラムの変換を改良した．この枠組みでは従来はデータとして整数とその１次元配列のみを扱うプログラムしか変換対象でなかった点を，より多くの種類のプログラムを変換して解析できる枠組みに拡張した．
論理制約付き項書換えシステムを対象とした定理自動証明ツールの開発として，これまでに本研究で開発してきたツールCtrlがビットベクトルを扱えるための理論定義ファイルを作成した．さらに，自動証明機能の改良を目的として試行錯誤を容易にするラッパーの開発に取り組んだ．このラッパーはCtrlの対話型証明機能には実装されていなかった補題候補の等式の追加を可能にした．さらに，対話証明の際に利用したコマンドの履歴に対して，改めてCtrlを実行する際に，ファイルに記載された履歴を自動実行したのちに対話証明を開始できる機能を追加した．これにより推論規則の適用戦略の開発のための試行錯誤が容易となり，実際に試行錯誤を行った結果，新たな補題候補の自動生成法を開発するに至った．新たな補題生成法を組み込んだ自動証明では，従来のCtrlが自動証明に成功していなかった例題の自動証明に成功した．
高信頼な検証法の開発に向けて，対話型定理証明支援系Isabelle/HOL上で論理制約付き項書換えシステムを形式化する課題にも着手した．論理制約付き項書換えシステムの形式化，整数上の簡単な命令型言語から論理制約付き項書換えシステムへの変換の形式化を完了した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の目的の一つは論理制約付き項書換えシステムへの変換と帰納法に基づく証明体系を命令型プログラムに応用し，命令型プログラムの新たな検証法の枠組みを確立することである．その目的に対し，変換対象となるプログラムの範囲を拡大したことは研究目的の達成に向けて順調に研究を遂行していると言える．さらに，ツールの開発および検証法の強化についても，これまでに開発してきたCtrlの機能を補完するラッパーの実装，それを利用した試行錯誤から新たな補題生成法を実現したことは当初の計画に実現性が十分にあることを示しており，初年度にこれらを達成できていることは研究目的を達成できることを十分に期待できる進捗状況であると言える．
一方，対話型定理証明支援系Isabelle/HOL上で提案手法を形式化することは2年目に取り組む予定であったが，当初の計画を順調に遂行できていたこと，さらに形式化は容易な課題ではなく時間を要する可能性が高いことから，初年度からIsabelle/HOL上での形式化に着手した．
以上のことから本研究の進行状況は概ね順調であると言える．
|
| Strategy for Future Research Activity |
Ctrlはプログラムの停止性や等価性を証明する上である程度，完成されたツールであるが，ビットベクトルなど新たなデータ構造を扱うには大幅な改修が必要であることがわかった．特に，ビットベクトルとその配列を扱うシステムを検証するには内部のデータ構造の改修が必要である．また，検証時にはSMTソルバを呼び出し，論理式の充足可能性や恒真性を証明するが，その際のデータのやり取りについては字句解析・構文解析を行いながら処理を進める．SMTソルバではSMT-LIBのような共通フォーマットがある一方で，その共通フォーマットは定期的に拡張される．その際にはCtrlの字句解析・構文解析を変更する必要がある．拡張性の高い検証ツールを開発することは，有用な検証システムの開発には必須であるため，これまでの研究の知見で得た特徴，必要な機能などを十分に検討し，定理自動証明器の開発に取り組む必要がある．これまでのCtrlを利用した検証実験から，定理自動証明に求められる機能，要件を精査し，拡張性のある検証システムを開発することをめざす．
一方で，推論規則の適用戦略や補題生成法の開発は本研究で目指す強力な検証システムの実現には不可欠である．そのために2年目以降も様々な例題に対して等価性や停止性の検証実験を行い，多くの知見を得ることに取り組む．また，高信頼性を保証するために，継続してIsabelle/HOL上での形式に取り組む．
|
Research Products
(9 results)
