2009 Fiscal Year Annual Research Report
ソフトウェアの安全性向上のための型理論の深化と応用
| Project/Area Number |
20240001
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
小林 直樹 Tohoku University, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
住井 英二郎 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Keywords | ソフトウェア検証 / 型理論 / モデル検査 / 高階再帰スキーム / 資源使用法解析 / ツリーオートマトン |
|---|
| Research Abstract |
本研究では、ソフトウェアの安全性向上のため、ソフトウェアを実行前に検証するための研究を行っている.本年度は、以下の成果が得られた.
1.高階再帰スキームに基づく関数型プログラムの検証手法の拡張
前年度に,関数型プログラムのさまざまな検証問題が高階再帰スキームと呼ばれる無限木を記述するための文法のモデル検査の問題に還元できることを示したが,このプログラム検証方式には,(1)プログラムが単純型システムで型付けされなければならない,(2)整数やリストなどの無限集合上のデータを扱えないという欠点があった.本年度は,リストや木構造処理プログラムの検証を可能にするために,高階木トランスデューサの一種であるHMTPを導入し,その検証問題を高階再帰スキームのモデル検査の問題に還元する手法を考案した.また,これによって、より広範囲の関数型プログラムの検証を行うための道筋が得られた.
2.型理論に基づく高階再帰スキームのモデル検査アルゴリズムの構築と実装
上記1のプログラム検証手法のためには、高階再帰スキームのモデル検査のアルゴリズムが必要であるが,従来知られていたアルゴリズムは極めて効率の悪く,実用には耐えないものだった.それに対し,本研究では典型的な入力に対しては効率よく動作するモデル検査アルゴリズムを考案,実装し,その有効性を示した.
また,高階再帰スキームのモデル検査の計算量について,従来の結果よりも精密な結果を得た.例えば,高階再帰スキームの生成する木が様相μ計算の論理式で表される性質を満たすか否かの判定問題の計算量は,いくつかのパラメタが定数であるという仮定のもとで,高階再帰スキームのサイズに対して多項式時間であることを示した.
3.メモリの使用法の検証のための型理論
C言語のプログラムにおいてfreeとmallocが正しく使われていること(具体的には2重に解放がおきない、mallocされたメモリ領域はプログラム終了時までに解放されるなどの性質)を検査するための検証器を作成し,その有効性を示した.
|
