2016 年度研究成果報告書

高階プログラミング言語で記述された大規模ソフトウェアの検証

研究課題

研究課題/領域番号	26330082
研究種目	基盤研究(C)
配分区分	基金
応募区分	一般
研究分野	ソフトウェア
研究機関	北陸先端科学技術大学院大学
研究代表者	寺内多智弘北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (70447150)
研究期間 (年度)	2014-04-01 – 2017-03-31
キーワード	プログラム検証 / モデル検査 / 高階関数 / 述語論理 / 型システム / 抽象詳細化 / 時相論理
研究成果の概要	本課題の目標は、関数型プログラミング言語など、高階関数を含むプログラミング言語で記述された大規模ソフトウェアに対して有効な自動検証手法の確立である。特に、近年、国内外において高く注目されている依存型型システムを用いたソフトウェアモデル検査による手法を研究した。主な研究成果は以下である：1.)よりよい抽象詳細化(ソフトウェアモデル検査に用いられる技術)の手法、2.)高階関数型プログラムのための停止性・活性仕様など時相論理仕様の自動検証手法。
自由記述の分野	ソフトウェア