2011 Fiscal Year Annual Research Report
| Project/Area Number |
23220001
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (S)
|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
篠原 歩 東北大学, 大学院・情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
|
|---|
| Keywords | 高階モデル検査 / プログラム検証 / データ圧縮 / 高階再帰スキーム / 型理論 |
|---|
| Research Abstract |
本研究では,高階モデル検査とそのプログラム検証やデータ圧縮への応用について研究することを目的としている.初年度である今年度は,その第一歩として,以下の3点について研究を行った.
1.高階モデル検査および関数型プログラム用検証器の改良
高階モデル検査と述語抽象化の技術を組み合わせ,関数型プログラミング言語MLのサブセット用の全自動プログラム検証器MoCHiを構築した.また,その基礎となる高階モデル検査の高速化のために,ゲーム意味論と型理論を組み合わせた新しい高階モデル検査アルゴリズムを考案し,モデル検査器GTRecSを実装した.
2.オブジェクト指向プログラムの自動検証のための高階モデル検査の拡張
高階モデル検査問題は,単純型付き関数型プログラムによって生成される無限木の性質を検証する問題であるが,オブジェクト指向プログラムの検証を扱うためには,単純型では不十分である.そこで,高階モデル検査問題自体を拡張し,再帰型の入ったプログラムによって生成される無限木の性質を扱えるようにした(以下「拡張高階モデル検査問題」と呼ぶ).拡張高階モデル検査問題は決定不能であることが以前の我々の研究によって知られているが,(完全ではないが)健全な手続きを与え,それに基づいて拡張高階モデル検査器の試作を行った.
3.高階モデル検査のデータ圧縮への応用
木構造データを,それを生成する関数型プログラムの形式で圧縮し,高階モデル検査を用いて圧縮したままの状態でデータの変換やパターンマッチングを行う手法を考案し,そのプロトタイプを実装した.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の3つの柱である,高階モデル検査の理論とアルゴリズムの発展,プログラム検証への応用,データ圧縮への応用について,それぞれ顕著な進展が得られ,それぞれFoSSaCS2011,PLDI2011,PEPM2012などに成果をまとめた論文が採択されている他,オブジェクト指向プログラムの検証への応用についてなど何件かの論文を執筆中である.
|
| Strategy for Future Research Activity |
3つの研究の柱についてこのまま順調に研究を進める.
研究自体は進んでいるが,今後の研究の進展に伴って重要性が増してくる実装や実験を補助する優秀な研究員の確保が(震災の影響もあって)やや難航しており,その点についての努力を続ける.
|
Research Products
(8 results)
