2012 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-05-31 – 2016-03-31
|
| Keywords | 高階モデル検査 / プログラム検証 / データ圧縮 / 型システム / 関数型言語 |
|---|
| Research Abstract |
本課題では、高階モデル検査とその応用について、(1)高階モデル検査の理論とそれに基づく高階モデル検査器の改良、(2)プログラム検証への応用、（３）データ圧縮への応用、の３つを柱として研究を進めている。以下、それぞれの柱について24年度から(繰越期間中の）25年度の実績を述べる。
（１）高階モデル検査の理論と実装：従来の高階モデル検査器TRecSの性能向上を行うとともに、新しい高階モデル検査アルゴリズムHorSatを考案し、その実装を行った。実験の結果、新しいモデル検査器HorSatは入力によってはTRecSの1000倍以上の性能向上を達成しており、これについては期待以上の成果が得られている。また、TRecSのアルゴリズムを拡張し、活性などの性質を扱えるモデル検査器APTRecSも構築した。さらに、高階モデル検査の対象である高階再帰スキーム(HORS)と呼ばれる高階文法の理論的性質についても調べ、HORSに対する反復補題などを証明した。
（２）プログラム検証への応用：高階モデル検査に基づく関数型プログラムの自動検証器MoCHiを拡張し、リストなどのデータ構造や例外などを用いたプログラムを自動検証できるようにした。さらに、前年度までの検証手法を改良し、必要に応じて関数に引数を追加することによって、背後に用いる論理体系に対する相対完全性を満たすような検証手法を確立した。また、前年度に考案したオブジェクト指向プログラムを自動検証するための手法の改良を行った。
（３）データ圧縮への応用：木構造データを、それを生成する関数型プログラムの形式で圧縮することにより、高階モデル検査を用いて圧縮したままデータの変換を行うことを目指している。２４～２５年度は、圧縮アルゴリズムの改良を行い、その結果、23年度時点よりもはるかに大きなデータの圧縮を現実的な時間で行うことが可能になった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
上記研究実績の概要で述べたとおり、各研究項目について順調に成果がでている。特に高階モデル検査アルゴリズムについては、大きな性能向上が得られており、期待以上の成果がでているともいえる。また、研究発表の項目に記載のように、コンピュータサイエンス分野全体のトップジャーナルであるJournal of the ACMに長編の論文が掲載されるなど、研究成果が国際的に高く評価されている。
|
| Strategy for Future Research Activity |
今後も計画どおりに研究を進める。プログラム検証やデータ圧縮への応用についても順調に研究は進んでいるものの、研究計画当初の最終目標の達成（例えば1000行規模の関数型プログラムの検証）にはまだ多くの課題が残されており、それらに関する取組を強化する予定である。
|
