2011 Fiscal Year Annual Research Report
項書換え系と木オートマトンに基づくプログラム安全性検証に関する研究
| Project/Area Number |
20300010
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| Keywords | 安全性 / 非干渉性 / 項書き換え系 / 木オートマトン / SMTソルバー |
|---|
| Research Abstract |
本研究の目的は,項書換え系や木オートマトンの解析技法を応用し,通信プロトコルを始めとするネットワークソフトウエアを含む並行プログラム一般の安全性について,効率的かつ適用範囲の広い検証技法を確立するとともに,検証システムを実装,評価することであり,今年度は次を研究実施計画とした.(1)抽象データ型の非干渉性に基づいたプログラムの安全性検証の枠組みの開発,(2)安全性検証への応用を目的としたプログラムのループ不変式自動発見手法の開発,(3)プログラムの安全性判定への等式理論を法とする充足可能性判定法の適用,(4)非干渉性をはじめとするプログラム安全性検証への応用を目指した項書き換え系と木オートマトン理論の展開.これに対して,以下のような成果を得た.
●プログラムのループ不変式自動発見手法の開発:関数呼出しを含むプログラムに対して,非線形不等式(関数呼出項も含む)の形のループ不変式を発見する手法を開発し,実験により評価した.
●充足可能性判定法の効率的実現:基本対称節と節の連言からなる論理式の充足可能性判定にリテラル監視法を取り入れて効率化した充足可能性判定ツールを開発し,その有効性を評価した.
●項書き換え系と木オートマトン理論の展開:停止性および到達可能性のそれぞれについて,それが決定可能である項書き換え系のクラスで,これまでに分かっているクラスより広いクラスを発見した.
|
