2016 Fiscal Year Annual Research Report
| Project/Area Number |
16J01038
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
寺尾 拓 東京大学, 情報理工学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2016-04-22 – 2019-03-31
|
| Keywords | プログラム検証 / 高階モデル検査 / 交差型システム / 述語抽象化 |
|---|
| Outline of Annual Research Achievements |
高階再帰スキームにプログラム変換することなく、直接値呼び高階ブーリアンプログラムをモデル検査するアルゴリズムを設計した。この手法では従来手法の「高階ブーリアンプログラムから高階再帰スキームへ変換する過程で発生するインスタンスの複雑化」という課題を解決することができる。直接的なモデル検査アルゴリズムはすでに提案されていたが、それは非現実的なアルゴリズムであった。本研究では、制御フロー情報を用いて型候補を削減することで効率の良いアルゴリズムを達成した。また、アルゴリズムの正当性を証明し、従来の高階再帰スキームに変換する手法に比べてスケーラビリティが改善することを実験によって確認した。この研究成果を論文としてまとめ、国際会議APLAS2016に投稿し、採択された。
次に、現状の関数型プログラム自動検証システムのさらなる効率改善のために、述語抽象化という過程におけるボトルネックを解決する方法の研究に着手した。そのボトルネックの原因は、入力プログラム中の整数などの無限ドメイン上のデータ型を有限ドメインであるブーリアン型に抽象化する過程で発生する、SMTソルバの多数の呼び出しである。その呼び出しを削減するために、抽象化とモデル検査を同時に行う融合アルゴリズムの開発に取り組んでいる。融合アルゴリズムを設計するにあたり、まず、無駄なSMTソルバの呼び出しがどの程度削減できるのかを調べるための予備実験を行なった。融合アルゴリズムをプロトタイプ実装し、関数型プログラム検証のベンチマークを用いて融合アルゴリズムと従来のアルゴリズムでのSMTソルバの呼び出し回数を比較したところ、融合アルゴリズムによって呼び出し回数を従来の15%程度に削減ができることがわかった。現在はアルゴリズムの定式化と完全な実装を進めている。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の研究計画に従い、プログラム変換を行わずにモデル検査を行う手法については手法の定式化・実装・評価を行い、国際会議APLAS2016で発表を行なった。次の述語抽象化とモデル検査の融合アルゴリズムについても定式化と実装を一定程度進めており、予備実験の結果からも成果が出る見通しは十分立っていると判断している。
|
| Strategy for Future Research Activity |
まずは、現在取り組んでいる、述語抽象化とモデル検査の融合アルゴリズムの定式化と実装を着々と進め、成果を論文として発表する。その後は、実装した検証システムを様々なベンチマークを用いて評価し、より幅広い関数型プログラムを現実的な時間で検証できるようにするための課題の洗い出しを行い、その解決方策について研究を行う。
|
