2015 Fiscal Year Final Research Report
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
|
| Keywords | 定理証明支援系 / ソフトウェア検証 |
|---|
| 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.
|
| Free Research Field |
情報理工学
|
