| 研究課題/領域番号 |
20240001
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
五十風 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
住井 英二郎 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| キーワード | ソフトウェア検証 / 型理論 / モデル検査 / 高階再帰スキーム / 資源使用法解析 / ツリーオートマトン |
|---|
| 研究概要 |
本研究では、ソフトウェアの安全性向上のため、ソフトウェアを実行前に検証するための型理論の研究を行っている.
本年度は、以下の成果が得られた.
1.高階再帰スキームに基づく関数型プログラムの検証
関数型プログラムの到達可能性検証(特定のプログラムポイントに制御が到達するか)や資源使用法の検証(ファイルやメモリが仕様どおりにアクセスされるか)などの問題が高階再帰スキームと呼ばれる無限木を記述するための文法のモデル検査の問題に還元できることを示した.これによって、再帰を含む単純型付き関数型プログラミング言語に対する健全かつ完全な検証手法が得られた.
2.高階再帰スキームのモデル検査のための型理論
上記1のプログラム検証手法のためには、高階再帰スキームのモデル検査のアルゴリズムが必要であるが、従来知られていたアルゴリズムは極めて複雑でかつ効率の悪いものだった.それに対し、型を用いることによって、ブッキ・オートマトンのある部分クラスで表される仕様については、文法のサイズに関して線形時間(ただし非終端記号の引数の数とオートマトンのサイズに対してはn-EXPTIME)でモデル検査を行うためのアルゴリズムが得られた.
3.メモリの使用法の検証のための型理論
C言語のようなfreeとmallocによって手動でメモリ管理をする言語において、freeとmallocが正しく使われていること(具体的には2重に解放がおきない、mallocされたメモリ領域はプログラム終了時までに解放されるなどの性質)を検証するための型システムを設計した.さらに、その型システムに基づき、Cプログラムにおけるfreeとmallocの使用法を自動検証するための検証器を作成した.
4.単調ACツリーオートマトンの表現力の研究
デッドロックの検証器TyPiCalの改良のために単調ACツリーオートマトンの表現力について研究を行い、単調ディオファンティン不等式とよばれる制約で表される言語はすべて単調ACツリーオートマトンによって表現できることを示した.
|
