2008 Fiscal Year Final Research Report
Verification of Software with Interactive Theorem Proving
| Project/Area Number |
18700018
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
MINAMIDE Yasuhiko University of Tsukuba, 大学院・システム情報工学研究科, 准教授 (50252531)
|
|---|
| Project Period (FY) |
2006 – 2008
|
| Keywords | ソフトウェア検証 / 定理証明系 / ホーア論理 |
|---|
| Research Abstract |
対話的定理証明によるソフトウェアの検証について、様々な角度から研究を行い、事例研究を通じ、小規模なソフトウェアやソフトウェアの核となる部分については、対話的定理証明による検証が可能であることを示した。特に、本研究の代表者が開発しているウェブプログラムの検証ツールPHP文字列解析器について、その核となるアルゴリズムの定式化・検証を行い、正当性を検証済みのプログラムを得ることに成功した。
|
Research Products
(12 results)
