Modular software verification with a proof assistant
| Project/Area Number |
25330096
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tsurumi University (2015)
National Institute of Informatics (2013-2014) |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HAGIYA Masami 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
YAMAMOTO Mitsuharu 千葉大学, 大学院理学研究科, 准教授 (00291295)
|
|---|
| Research Collaborator |
YUASA Yoshifumi
HENMI Ko
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2013: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 定理証明支援系 / ソフトウェア検証 / ディペンダブル・コンピューティング / Coq / 型推論 / コード抽出 |
|---|
| Outline of Final Research Achievements |
We have implemented code extraction from proof assistant Coq to programming language Scala. Once a proof is given to a code written in Coq, then the extracted code is guaranteed that it behaves correctly. There are many working systems written in Java, and Scala code is easily integrated with them because it runs on Java VM. Our code itself is originally written in Coq and is extracted from a proof on Coq that it works correctly.
|
Report
(4 results)
Research Products
(18 results)
