| 研究実績の概要 |
本研究の大目標は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした. 以上により進捗はおおむね良好であるといえる.
|
| 今後の研究の推進方策 |
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装する研究をさらに進める. ループ解析の精度が必要であることがわかってきたので, 抽象解釈の技法を取り入れてループ解析を高精度化する.
|
