| 研究課題/領域番号 |
15K12013
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
|
|---|
| 研究分担者 |
田中 哲 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (10357452)
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| 研究課題ステータス |
完了 (2017年度)
|
| 配分額 *注記 |
2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
2017年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2016年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2015年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 定理証明支援系 / 簡潔データ構造 / プログラミング言語OCaml / プログラミング言語C / コード生成器 |
|---|
| 研究成果の概要 |
インターネットに接続される機器の増加に伴い、蓄積されるデータが爆発的に増大している。これらの大規模なデータを解析し、活用しようという動きが、いわゆる「ビッグデータ」のもとで進んでいる。しかし、ビッグデータ処理に用いられるプログラムの信頼性について、十分に厳密な検討や検証がなされているとは言いがたい。本研究では、「簡潔データ構造」に着目し、そのアルゴリズム及び実装の安全な開発方法を提案し、評価を行った。具体的には、定理証明支援系Coqを用いて、簡潔データ構造の基本的なアルゴリズムを形式化し、その性質を検証してから、実用的なコードを出力できるようにした。
|
