Towards formal verification of big data processing
| Project/Area Number |
15K12013
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
AFFELDT Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田中 哲 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (10357452)
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2017: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2016: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2015: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 定理証明支援系 / 簡潔データ構造 / プログラミング言語OCaml / プログラミング言語C / コード生成器 |
|---|
| Outline of Final Research Achievements |
Data accumulate as the result of the increasing number of devices connected to the Internet. These so-called big data are the object of various analyses whose reliability is important. In this project, we focus on succinct data structures as an example of big data. We propose and evaluate an approach for their safe implementation. Concretely, we formalize and verify standard algorithms for succinct data structures using the Coq proof-assistant, and extend the latter so as to be able to extract safe programs that are usable in practice.
|
Report
(4 results)
Research Products
(16 results)
