2017 Fiscal Year Annual Research Report
Towards formal verification of big data processing
| Project/Area Number |
15K12013
|
|---|
| 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
|
| Keywords | 定理証明支援系 / 簡潔データ構造 / プログラミング言語C / コード生成器 |
|---|
| Outline of Annual Research Achievements |
平成29年度、昨年度提案したコード生成の手法を実用的な応用に適用し、簡潔データ構造の基礎の形式化を拡張した。平成28年度に提案したコード生成の手法（monomorphizationというプログラム変換に基づくC言語のコード生成器とmonadificationというプログラム変換器）の開発を進め、応用例に適用した。特に、平成27年度に形式検証したrankアルゴリズムに適用した。その結果として、C言語のコードで記述された実用的な実装を得られ、その正しさもmonadという概念を用いて確認した。また、同じmonadの概念を用いて、正しさ以外の性質（計算量など）も形式的に検証できた。以上の生成器と変換器は定理証明支援系Coqのプラグインとして実現しており、これをオープンソースコードとして配布した。その成果を国内ワークショップで発表し、雑誌論文として投稿し、採択され、招待講演として国際ワークショプで発表した。また、上記のコード生成器を最適化で拡張した。具体的には、C言語で記述された実装の効率改善のため、linearity解析を実装した。また、平成27年度で開始した簡潔データ構造の基礎の形式化を拡張した。具体的には、select関数とその性質およびLOUDS木という代表的な簡潔データ構造とその性質を形式化した。以上のlinearity解析による最適化
と簡潔データ構造の形式化を国内ワークショップでポスターとして発表した。
|
