2016 Fiscal Year Research-status Report
| 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 |
平成28年度、簡潔データ構造の基礎的なアルゴリズムの形式検証実験を完成させ、論文を作成し投稿、その成果を国際学会で発表した。検証したrankアルゴリズムは最小のメモリを使用し、効率的にビット列内のビットを数えるアルゴリズムである。本実験は、定理証明支援系Coqのコード出力機能を用いて、検証済みかつ実行可能なプログラムを形式モデルから得られた。平成28年度は特に、得られたプログラムのデータ構造の単純化と最適化に集中した。しかし、そのプログラムは主に関数型言語OCamlで記述されていたため、効率に関して改善の余地があった。従って、さらに効率の良いプログラムを得られるように、Coqのコード出力の新機能を提案した。本提案によって、形式モデルから直接効率の良い低レベルのC言語のプログラムを得られ、そのプログラムと元の形式モデルの適切さを確認するため、新しい仕組みを提案した。具体的に、Coqプラグインという拡張方法を用いて、C言語のプログラムの生成器(monomorphizationという型を特化する仕組みかつC言語のコード生成の仕組み)のプロトタイプを実装した。その生成器の安全性を確認するため、monadificationというプログラム変換もCoqプラグインとして実装した。以上のプラグインを合わせて、形式的に安全性を確かめられる生成器ができた。その生成器のプロトタイプの実験について国内ワークショップでポスターを発表し、議論した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成28年度、検証済みの簡潔データ構造のプログラムの効率化に努めた結果で、実用的かつ独創的なアプローチの提案ができたため、簡潔データ構造のアルゴリズムの形式検証のベースができた。
|
| Strategy for Future Research Activity |
平成28年度に提案したコード出力機能を向上し、その機能について論文を作成し、投稿する。それから、平成27年度に提案した定理群を拡張し、検証方法を簡潔データ構造のselectアルゴリズムと簡潔木に適用する。
|
| Causes of Carryover |
形式検証の国際会議は日本で行われたため、未使用額が生じた。
|
| Expenditure Plan for Carryover Budget |
論文を投稿するので、その成果発表に伴う旅費や参加費として利用する。
|
