2015 年度研究成果報告書

ゲーム意味論に基づくリファインメント型の拡張とその応用

研究課題

研究課題/領域番号	25730035
研究種目	若手研究(B)
配分区分	基金
研究分野	ソフトウェア
研究機関	筑波大学
研究代表者	海野広志筑波大学, システム情報系, 助教 (80569575)
研究期間 (年度)	2013-04-01 – 2016-03-31
キーワード	プログラム検証 / 型システム / 定理自動証明 / 制約解消
研究成果の概要	本研究では、ソフトウェアの信頼性向上のために、高レベルプログラムの形式検証手法の一つであるリファインメント型システムおよびその型検査・推論法の、表示的意味論に基づく拡張を目指した。その主な成果として、代数データ構造を扱う高階関数型プログラムの(a)停止性、(b)非停止性、(c)関係的性質の全自動・高精度検証が可能な検証ツールRCamlの開発が挙げられる。
自由記述の分野	情報科学