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
|
| Project Status |
Completed (Fiscal Year 2008)
|
| Budget Amount *help |
¥3,400,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥300,000)
Fiscal Year 2008: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2007: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2006: ¥1,100,000 (Direct Cost: ¥1,100,000)
|
|---|
| Keywords | ソフトウェア検証 / 定理証明系 / ホーア論理 / Hoare論理 / 対話的定理証明 / プログラム解析 |
|---|
| Research Abstract |
対話的定理証明によるソフトウェアの検証について、様々な角度から研究を行い、事例研究を通じ、小規模なソフトウェアやソフトウェアの核となる部分については、対話的定理証明による検証が可能であることを示した。特に、本研究の代表者が開発しているウェブプログラムの検証ツールPHP文字列解析器について、その核となるアルゴリズムの定式化・検証を行い、正当性を検証済みのプログラムを得ることに成功した。
|
Report
(4 results)
Research Products
(20 results)
