2014 Fiscal Year Annual Research Report
| Project/Area Number |
23220001
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
小林 直樹 東京大学, 情報理工学(系)研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報工学研究科(系), 助教 (80569575)
|
|---|
| Project Period (FY) |
2011-04-01 – 2016-03-31
|
| Keywords | 高階モデル検査 / プログラム検証 / 高階文法 / データ圧縮 |
|---|
| Outline of Annual Research Achievements |
本課題では、高階モデル検査とその応用について、（１）高階モデル検査の理論とそれに基づく高階モデル検査器の構築、（２）プログラム検証への応用、（３）データ圧縮への応用、を３つの柱として研究している。以下、それぞれについて２６年度（ただし２５年度繰り越し期間分として報告済みの内容は除く）から繰越期間中の２７年度の実績を述べる。
（１）高階モデル検査の理論：高階モデル検査器の高速化のため、ZDDを用いて共通型および型環境を表現するアルゴリズムを考案・実装した。実験により、文法サイズに対してほぼ線形時間で動作し、大きな入力に対しては既存の高階モデル検査器よりも高速であることを確認した。また、高階モデル検査の検証対象である高階文法の性質に関する研究を引き続き行った。
（２）プログラム検証への応用：(i)２つの関数の等価性などの複数の関数間の関係、(ii)高階関数型プログラムの非停止性（与えられたプログラムがある入力に対して無限実行列を持つこと）、などこれまで扱えなかった性質の自動検証を高階モデル検査を用いて行う手法を考案し、実装・評価を行った。前者は、高階の改良型の検証問題を一階の改良型の検証問題に帰着することで、後者は、過大抽象化と過小抽象化を組み合わせることで実現した。また、高階モデル検査に基づくプログラム自動検証で必要となる、述語発見手法の改良を行った。
（３）データ圧縮への応用：木構造データを、それを生成する関数型プログラムの形で圧縮する方式について、既存アルゴリズムの改良を行い、入力データのサイズに対してほぼ線形時間で動作するアルゴリズムを考案・実装し、実験により期待通りの動作をすることを確認した。
|
| Research Progress Status |
27年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
27年度が最終年度であるため、記入しない。
|
