| 研究概要 |
本研究の目的は,項書換え系や木オートマトンの解析技法を応用し,通信プロトコルを始めとするネットワークソフトウエアを含む並行プログラム一般の安全性について,効率的かつ適用範囲の広い検証技法を確立するとともに,検証システムを実装,評価することである.
今年度行なった主な研究は以下のとおりである.
・ 抽象データ型の非干渉性に関する研究:従来の情報流解析によるプログラムの安全性は,メモリーの非干渉性に依存している.本研究では,メモリーを一般化した抽象データ型の非干渉性を定式化し,その検証法を考察した.
・ 等式理論を法とするDPLL遷移系の提案と実装:プログラム検証の問題は,与えられた等式理論の下での論理式の充足可能性問題に帰着されることが多い.本研究では,与えられた等式理論と論理式に対して,自動的にその等式理論の決定手続きを生成し,論理式の等式理論を法とする充足可能性を判定する枠組みを提案し,その実装,評価を行った.
その他に,木オートマトンの受理する言語の閉包性の研究,項書き換え系の停止性に関する研究,制約付き項書換え系の性質自動証明に関する研究を行なった.
|
