2016 Fiscal Year Annual Research Report
Refinement and Extension of Higher-Order Model Checking
| Project/Area Number |
15H05706
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2015-05-29 – 2020-03-31
|
| Keywords | 高階モデル検査 / プログラム検証 / 高階文法 / データ圧縮 |
|---|
| Outline of Annual Research Achievements |
本課題では、高階モデル検査の（１）理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、（２）プログラム検証への応用、（３）高階モデル検査の拡張とそのプログラム検証への応用、（４）データ圧縮への応用、の４つを柱に研究を進めている。以下、それぞれの項目について、平成28年度（およびその繰越として遂行した平成29年度の一部の結果）について述べる。
（１）理論的基盤の強化：HORSモデル検査とHFLモデル検査という2種類の高階モデル検査の間に相互変換が存在することを示すとともに、HFLモデル検査問題を型推論問題に帰着できることを示した。後者の結果に基づき、HFLモデル検査器のプロトタイプを作成した。また、高階文法の性質について調べ、語を生成するオーダーnの文法と木文法を生成するオーダーn-1の文法と間の対応関係を示した。さらに、高階モデル検査アルゴリズムの改良を行い、値呼びプログラムに対して直接的に高階モデル検査を適用する手法を考案、実装した。
（２）プログラム検証への応用：プログラム検証で扱える対象プログラムや性質の拡充を行い、関数型プログラムの公平非停止性の検証、コード生成プログラムの検証、動的なスレッド生成を伴う高階並列プログラムの検証、などを可能にした。
（３）拡張高階モデル検査：HORSに再帰型を加えて拡張したμHORSに対するモデル検査アルゴリズムの改良を行い、その有効性をJavaプログラムの検証を通して示した。
（４）データ圧縮への応用：データをそれを生成する関数型プログラムの形に圧縮する方式（高階圧縮）について、圧縮後のプログラムをビット列に変換する部分の改良を行った。また、高階圧縮のための様々な要素技術について研究を進めた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
トップ国際会議POPLに論文が採択されるなど順調に研究成果が出ている。特に、POPL 2017で発表した成果は、当初想定していなかった2種類の高階モデル検査の相互の関係を明らかにしたものであり、高階モデル検査およびそのプログラム検証について新しい展望が開けた。
|
| Strategy for Future Research Activity |
引き続き研究計画にそって研究を進めるが、研究の柱(3)の拡張高階モデル検査については、新しく得られた2種類の高階モデル検査同士の関係に関する結果の発展を優先させる。
|
