| 研究課題/領域番号 |
15K12013
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
|
|---|
| 研究分担者 |
田中 哲 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (10357452)
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 定理証明支援系 / 簡潔データ構造 / プログラミング言語C / コード生成器 |
|---|
| 研究実績の概要 |
平成28年度、簡潔データ構造の基礎的なアルゴリズムの形式検証実験を完成させ、論文を作成し投稿、その成果を国際学会で発表した。検証したrankアルゴリズムは最小のメモリを使用し、効率的にビット列内のビットを数えるアルゴリズムである。本実験は、定理証明支援系Coqのコード出力機能を用いて、検証済みかつ実行可能なプログラムを形式モデルから得られた。平成28年度は特に、得られたプログラムのデータ構造の単純化と最適化に集中した。しかし、そのプログラムは主に関数型言語OCamlで記述されていたため、効率に関して改善の余地があった。従って、さらに効率の良いプログラムを得られるように、Coqのコード出力の新機能を提案した。本提案によって、形式モデルから直接効率の良い低レベルのC言語のプログラムを得られ、そのプログラムと元の形式モデルの適切さを確認するため、新しい仕組みを提案した。具体的に、Coqプラグインという拡張方法を用いて、C言語のプログラムの生成器(monomorphizationという型を特化する仕組みかつC言語のコード生成の仕組み)のプロトタイプを実装した。その生成器の安全性を確認するため、monadificationというプログラム変換もCoqプラグインとして実装した。以上のプラグインを合わせて、形式的に安全性を確かめられる生成器ができた。その生成器のプロトタイプの実験について国内ワークショップでポスターを発表し、議論した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
平成28年度、検証済みの簡潔データ構造のプログラムの効率化に努めた結果で、実用的かつ独創的なアプローチの提案ができたため、簡潔データ構造のアルゴリズムの形式検証のベースができた。
|
| 今後の研究の推進方策 |
平成28年度に提案したコード出力機能を向上し、その機能について論文を作成し、投稿する。それから、平成27年度に提案した定理群を拡張し、検証方法を簡潔データ構造のselectアルゴリズムと簡潔木に適用する。
|
| 次年度使用額が生じた理由 |
形式検証の国際会議は日本で行われたため、未使用額が生じた。
|
| 次年度使用額の使用計画 |
論文を投稿するので、その成果発表に伴う旅費や参加費として利用する。
|
