| 研究課題/領域番号 |
15H05706
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2015-05-29 – 2020-03-31
|
| キーワード | 高階モデル検査 / プログラム検証 / 高階文法 / データ圧縮 |
|---|
| 研究実績の概要 |
本課題では、高階モデル検査の（１）理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、（２）プログラム検証への応用、（３）高階モデル検査の拡張とそのプログラム検証への応用、（４）データ圧縮への応用、の４つを柱に研究を進めている。以下、それぞれの項目について、平成28年度（およびその繰越として遂行した平成29年度の一部の結果）について述べる。
（１）理論的基盤の強化：HORSモデル検査とHFLモデル検査という2種類の高階モデル検査の間に相互変換が存在することを示すとともに、HFLモデル検査問題を型推論問題に帰着できることを示した。後者の結果に基づき、HFLモデル検査器のプロトタイプを作成した。また、高階文法の性質について調べ、語を生成するオーダーnの文法と木文法を生成するオーダーn-1の文法と間の対応関係を示した。さらに、高階モデル検査アルゴリズムの改良を行い、値呼びプログラムに対して直接的に高階モデル検査を適用する手法を考案、実装した。
（２）プログラム検証への応用：プログラム検証で扱える対象プログラムや性質の拡充を行い、関数型プログラムの公平非停止性の検証、コード生成プログラムの検証、動的なスレッド生成を伴う高階並列プログラムの検証、などを可能にした。
（３）拡張高階モデル検査：HORSに再帰型を加えて拡張したμHORSに対するモデル検査アルゴリズムの改良を行い、その有効性をJavaプログラムの検証を通して示した。
（４）データ圧縮への応用：データをそれを生成する関数型プログラムの形に圧縮する方式（高階圧縮）について、圧縮後のプログラムをビット列に変換する部分の改良を行った。また、高階圧縮のための様々な要素技術について研究を進めた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
トップ国際会議POPLに論文が採択されるなど順調に研究成果が出ている。特に、POPL 2017で発表した成果は、当初想定していなかった2種類の高階モデル検査の相互の関係を明らかにしたものであり、高階モデル検査およびそのプログラム検証について新しい展望が開けた。
|
| 今後の研究の推進方策 |
引き続き研究計画にそって研究を進めるが、研究の柱(3)の拡張高階モデル検査については、新しく得られた2種類の高階モデル検査同士の関係に関する結果の発展を優先させる。
|
