2022 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 |
本研究の大目標は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して,精密なメモリモデルの理論および再帰データ, 間接参照を追加した論理体系をまず構築し, これをほぼ実装した. また, この理論全体に関連して, 循環証明体系の計算の複雑性を明らかにした. 以上により進捗はおおむね良好であるといえる.
|
| Strategy for Future Research Activity |
オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系に対して, 再帰呼出し, 再帰データ, 関数ポインタを追加し, 大規模なシステムソフトウェアを解析/検証する}ことができる理論を確立し, その理論に基づいて解析/検証システムをパソコン上に実装する研究をさらに進める. ループ解析の精度が必要であることがわかってきたので, 抽象解釈の技法を取り入れてループ解析を高精度化する.
|
-
-
-
-
[Journal Article] 帰納法に関する推論の計算複雑性2023
Author(s)
伊藤 宗平, 龍田 真
-
Journal Title
Proceedings of the 24th JSSST Workshop on Programming and Programming Languages (PPL2023)
Volume: 1
Pages: 1--15
Peer Reviewed
-
