| 研究課題/領域番号 |
15K12013
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
|
|---|
| 研究分担者 |
田中 哲 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (10357452)
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 定理証明支援系 / 簡潔データ構造 / プログラミング言語OCaml |
|---|
| 研究実績の概要 |
平成27年度、簡潔データ構造の基礎を形式化し、基礎的なアルゴリズムの形式検証に成功した。まず、定理証明支援系Coqを用いて、簡潔データ構造の基礎となるrank関数などを抽象的に定義し、その性質の証明に取り組み、定理群の開発を開始した。特に、アルゴリズムが利用するメモリ量に関する性質に集中した。また、検証済みで実用的なrank関数を得るため、定理証明支援系Coqを用いた検証方法を提案し、検証実験を行った。簡潔データ構造は低レベルな操作を利用するため、通常の実装の検証は困難である。具体的には、抽象的なrankアルゴリズムを検証してから、CoqのExtraction機能を用いて、OCaml言語の実装を出力した。但し、効率のいいコードが得られるように、ビット列を表現するOCamlライブラリを新しく構築した。特に、このライブラリは最新のIntelアーキテクチャの命令を利用する。以上の実験に関する論文を国内ワークショップに投稿し、採択され、本ワークショップの論文賞を受賞した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
平成27年度、簡潔データ構造に関する実装はビット列のレベルで実現し、実用的な実装を得たので、本プロジェクトの目的の一つを達成した。
|
| 今後の研究の推進方策 |
平成２７年度の成果を向上し、国際会議に投稿あるいは雑誌論文を作成する。平成２７年度に提案した検証方法を簡潔データ構造のselectアルゴリズムに適用する。提案した定理群を拡張あるいは整理と拡張する。MathCompの実数を利用できるように移植する。簡潔木の形式化を開始する。
|
| 次年度使用額が生じた理由 |
名古屋で会議を行わなかったので、未使用額が生じた。計画の変更によって、購入予定の書籍を遅らせた。
|
| 次年度使用額の使用計画 |
国際会議に論文を投稿するので、その旅費と参加費として利用する。形式検証を加速するため、プロジェクトメンバーの開発会議を増やす。
|
