| Project/Area Number |
18H03226
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
Tatsuta Makoto 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥16,900,000 (Direct Cost: ¥13,000,000、Indirect Cost: ¥3,900,000)
Fiscal Year 2020: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000)
Fiscal Year 2019: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000)
Fiscal Year 2018: ¥5,980,000 (Direct Cost: ¥4,600,000、Indirect Cost: ¥1,380,000)
|
|---|
| Keywords | ソフトウェア検証 / ソフトウェア解析 / 分離論理 / メモリ安全性 / プログラム論理 |
|---|
| Outline of Final Research Achievements |
The purpose of this research is to deepen O'Hearn's theory to establish new theory for more precise software verification. The results of this research is to define a logical system which is obtained by adding general inductive definitions, arrays, and arithmetic to O'Hearn's theory, and present efficient algorithm for theorem proving, biabduction, and loop invariant generation for the logical system, prove the correctness and the decidability of these algorithms, and showed evidence for efficiency of these algorithms by implementation and experiments. By this implementation, we proved the safety of several programs.
|
| Academic Significance and Societal Importance of the Research Achievements |
オハーン理論は分離論理を用いたメモリ安全性の自動検証理論として理論的にも実用的にも成功したが、一方でそれは精度が不十分であった. 本研究は, オハーン理論をより高精度な自動検証ができるように発展させた理論が何であるか明らかにでき、学術的意義が高い.
航空機, 銀行オンラインシステムなど, ソフトウェアは社会的に重要な役割を担っている. 一方では, ソフトウェアは今だに人手で生産されている. このため, 高信頼ソフトウェアの生産は大問題である. 本研究は, ソフトウェア検証の理論を発展させることにより, これらの問題の解決をすすめることができ、社会的意義が大きい.
|
