| 研究概要 |
本研究では,高階モデル検査とそのプログラム検証やデータ圧縮への応用について研究することを目的としている.初年度である今年度は,その第一歩として,以下の3点について研究を行った.
1.高階モデル検査および関数型プログラム用検証器の改良
高階モデル検査と述語抽象化の技術を組み合わせ,関数型プログラミング言語MLのサブセット用の全自動プログラム検証器MoCHiを構築した.また,その基礎となる高階モデル検査の高速化のために,ゲーム意味論と型理論を組み合わせた新しい高階モデル検査アルゴリズムを考案し,モデル検査器GTRecSを実装した.
2.オブジェクト指向プログラムの自動検証のための高階モデル検査の拡張
高階モデル検査問題は,単純型付き関数型プログラムによって生成される無限木の性質を検証する問題であるが,オブジェクト指向プログラムの検証を扱うためには,単純型では不十分である.そこで,高階モデル検査問題自体を拡張し,再帰型の入ったプログラムによって生成される無限木の性質を扱えるようにした(以下「拡張高階モデル検査問題」と呼ぶ).拡張高階モデル検査問題は決定不能であることが以前の我々の研究によって知られているが,(完全ではないが)健全な手続きを与え,それに基づいて拡張高階モデル検査器の試作を行った.
3.高階モデル検査のデータ圧縮への応用
木構造データを,それを生成する関数型プログラムの形式で圧縮し,高階モデル検査を用いて圧縮したままの状態でデータの変換やパターンマッチングを行う手法を考案し,そのプロトタイプを実装した.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究の3つの柱である,高階モデル検査の理論とアルゴリズムの発展,プログラム検証への応用,データ圧縮への応用について,それぞれ顕著な進展が得られ,それぞれFoSSaCS2011,PLDI2011,PEPM2012などに成果をまとめた論文が採択されている他,オブジェクト指向プログラムの検証への応用についてなど何件かの論文を執筆中である.
|
