2010 Fiscal Year Annual Research Report
ソフトウェアの安全性向上のための型理論の深化と応用
| Project/Area Number |
20240001
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
住井 英二郎 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
松田 一孝 東北大学, 大学院・情報科学研究科, 助教 (10583627)
|
|---|
| Keywords | ソフトウェア検証 / 型理論 / 高階モデル検査 / 述語抽象化 / メモリ使用法解析 |
|---|
| Research Abstract |
本研究では、ソフトウェアの安全性向上のため、ソフトウェアを実行前に検証するための研究を行っている.本年度は、以下の成果が得られた.
1.高階モデル検査に基づく関数型プログラムの検証手法の拡張
高階モデル検査に基づく関数型言語の検証手法で整数などの無限集合上のデータを扱えるようにするため,述語抽象化と反例からの述語発見の手法を導入し,MLのごく小さなサブセットに対してプログラムを自動検証することができるツールMoCHiを作成した.また,前年度に考案した高階木トランスデューサHMTTの検証手法を拡張し,木構造データに関する不変条件による注釈が与えられているという条件つきで(HMTTという制限のない)任意の木構造処理プログラムの自動検証を可能にした.
2.新しい高階モデル検査アルゴリズムの開発
上記1のプログラム検証手法の基礎となっているのは高階モデル検査であるが,そのための新しいアルゴリズムを考案した.従来知られていたものは,(1)実験的には多くの入力に対して効率よく動作するが,最悪の場合には入力となる文法のサイズに対して多重指数関数時間がかかるもの,(2)理論的には文法のサイズに対して線形時間だが係数が大きすぎて現実には使えないもの,の2種類しかなかった.それに対し,新しいアルゴリズムは,(他のパラメタを固定するという条件の下で)入力文法のサイズに対して線形時間でかつ実験的にも効率よく動作することが確かめられた.
3.メモリ使用法検証器FreeSafeTyの改良
前年度までに構成したC言語のプログラムにおけるfreeとmallocの使用法を検証するためのツールFreeSafeTyではエイリアス情報に関する注釈が必要だったが,mustエイリアス解析を組み合わせることにより,全自動で検証できるようにした.
|
