2021 Fiscal Year Annual Research Report
| Project/Area Number |
21H03421
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Keywords | 分離論理 / ソフトウェア検証 |
|---|
| Outline of Annual Research Achievements |
本研究の大目標は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,再帰呼出しを追加した論理体系をまず構築し, これをほぼ実装した. このために, 配列のある記号ヒープのエンテイルメントの判定器の理論を構築し, この判定器の正当性性を証明し, パソコン上に実装して実験を行い, 理論の有効性を示した. また, Cプログラムからプログラムの同等性を保って関数ポインタを除去するアルゴリズムを提案し, これをパソコン上に実装して実験を行い, アルゴリズムの有効性を示した.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,再帰呼出しを追加した論理体系をまず構築し, これをほぼ実装した. このために, 配列のある記号ヒープのエンテイルメントの判定器の理論を構築し, この判定器の正当性性を証明し, パソコン上に実装して実験を行い, 理論の有効性を示した. また, Cプログラムからプログラムの同等性を保って関数ポインタを除去するアルゴリズムを提案し, これをパソコン上に実装して実験を行い, アルゴリズムの有効性を示した. また配列とリストをもつ分離論理における両仮説形成アルゴリズムを提案し, その正当性を証明し, これをパソコン上に実装して実験を行った. 以上により進捗はおおむね良好であるといえる.
|
| Strategy for Future Research Activity |
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装する研究をさらに進める.ループ解析の精度が必要であることがわかってきたので, 抽象解釈の技法を取り入れてループ解析を高精度化する.
|
