研究課題
本研究では、高レベルプログラムの検証のための形式体系であるリファインメント型システムおよびその型検査・型推論法を拡張することによって、既存手法で扱えなかった言語機能・仕様を検証可能とすることを目指した。本年度は以下の成果を得た。1. リファインメント型最適化：従来のリファインメント型推論問題を、多目的最適化問題として一般化したリファインメント型最適化問題を提案し、実際にそのような最適化問題を解くための、ホーン節制約最適化に基づく新手法を開発した。これによって、高レベルプログラムの、実行が停止しない入力条件の推論や、最悪の計算ステップ数を引き起こす入力条件の推論といった新しい応用が可能になった。2. 完全正当性検証：部分正当性に加えて停止性を検証可能なようにリファインメント型システムを拡張し、その型推論問題を整礎性制約付きのホーン節制約解消問題に帰着・解消する手法を提案した。3. 再帰データ構造の検証：再帰データ構造を扱うプログラムの部分正当性・完全正当性検証を可能とするための拡張を、リファインメント型システムと型推論法に対して行った。
すべて 2016 2015
すべて 雑誌論文 (3件) (うち査読あり 3件、 謝辞記載あり 3件) 学会発表 (5件) (うち国際学会 4件、 招待講演 1件)
Proceedings of POPL 2016
巻: なし ページ: 57-68
10.1145/2837614.2837667
Proceedings of SAS 2015, LNCS
巻: 9291 ページ: 199--216
10.1007/978-3-662-48288-9_12
Proceedings of APLAS 2015, LNCS
巻: 9458 ページ: 295-312
10.1007/978-3-319-26529-2_16
