| 研究成果の概要 |
本研究の目的は, オハーン理論を発展させることにより高精度なソフトウェア検証を可能にする新理論を構築することであった. 研究成果は, オハーン理論に一般帰納的述語, 配列, 算術を追加した論理体系を定義し, その論理体系に対して, 定理証明, 両仮説形成, 記号計算のループインバリアント生成の三つを計算する効率よいアルゴリズムを与え, それらのアルゴリズムの正しさおよび決定可能性を数学的に証明し, またそれらのアルゴリズムの効率を実装実験により証拠付けた. この実装システムを用いていくつかのプログラムの安全性を検証した.
|
| 研究成果の学術的意義や社会的意義 |
オハーン理論は分離論理を用いたメモリ安全性の自動検証理論として理論的にも実用的にも成功したが、一方でそれは精度が不十分であった. 本研究は, オハーン理論をより高精度な自動検証ができるように発展させた理論が何であるか明らかにでき、学術的意義が高い.
航空機, 銀行オンラインシステムなど, ソフトウェアは社会的に重要な役割を担っている. 一方では, ソフトウェアは今だに人手で生産されている. このため, 高信頼ソフトウェアの生産は大問題である. 本研究は, ソフトウェア検証の理論を発展させることにより, これらの問題の解決をすすめることができ、社会的意義が大きい.
|
