| 研究課題/領域番号 |
15H05706
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 助教 (80569575)
|
|---|
| 研究期間 (年度) |
2015-05-29 – 2020-03-31
|
| キーワード | 高階モデル検査 / プログラム検証 / 高階文法 / データ圧縮 |
|---|
| 研究実績の概要 |
本課題では、高階モデル検査の（１）理論とモデル検査アルゴリズム、（２）プログラム検証への応用、（３）データ圧縮への応用について研究を進めている。以下、それぞれについて、平成27年度の研究実績を述べる。
（１）高階モデル検査の理論とモデル検査アルゴリズム：高階モデル検査アルゴリズムおよびその実装の改良を行った。その結果得られた新しい高階モデル検査器HorSat2は、標準のベンチマークについて従来の最速のモデル検査器よりも平均10倍程度の高速化を達成でき、単純な入力であれば数十万行の文法であっても一分程度で処理できる（従来の最速のモデル検査器では一万行程度が限界）ことを確認した。
（２）プログラム検証への応用：高階モデル検査に基づくプログラム検証の新しい応用として、プログラム等価性、公平停止性の検証手法の考案および実装を行った。後者については、公平停止性の検証を到達可能性問題に帰着する手法を考案し、昨年度までに構築ずみの高階モデル検査に基づく到達可能性問題検証器と組み合わせることによって公平停止性検証器を実装した。これにより、線形時相論理LTLで表現可能な任意の性質の自動検証が可能になった。また、プログラムの検証を関数単位に分割して検証することを可能にするため、詳細型検査問題を到達可能性問題に帰着して解く手法を考案・実装した。さらに、木構造処理プログラムの自動検証手法やホーン節に基づく詳細型推論手法の改良を行った。
（３）データ圧縮への応用：木構造データを、それを生成する関数型プログラム（ラムダ式）の形に圧縮する方式について、得られたラムダ式をコンパクトなビット列に変換する方法について引き続き改良を行い、（より表現力の弱い体系なので原理的にはよりコンパクトな表現が可能である）straightline programのビット表現と遜色ない大きさのビット表現を得ることに成功した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
トップ国際会議POPLに論文が採択されるなど順調に研究成果が出ている。また、高階モデル検査器についても大幅な高速化を達成できた。
|
| 今後の研究の推進方策 |
引き続き計画に従って研究を進める。
関数型プログラムの検証手法の研究が進んでいる一方、オブジェクト指向プログラムの検証の研究の進展がやや遅れており、アプローチの見直しも含めて検討する。
|
