| 研究課題/領域番号 |
26330082
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | ソフトウェア検証 / モデル検査 / 高階関数 / 述語論理 / 抽象詳細化 / 時相論理 |
|---|
| 研究実績の概要 |
1. ソフトウェアモデル検査など、近代のソフトウェア検証手法の基盤技術である、述語抽象における「述語抽象詳細化」に関する研究を行った。述語抽象詳細化では抽象モデル検査で得られた偽反例などを用い検証に役立つ述語を推論する。この研究に関して、以下の成果を得た。(a)反復的なサンプリングを用いた「単純な」述語の推論手法。(b)ある仮定のもと、検証プロセスが収束する保証のある抽象詳細化の手法。(c)推論される述語の大きさと検証プロセスの効率の相関性に関する理論的研究。(a), (b), (c)の成果をまとめた論文をそれぞれ国際会議TACAS 2015, ESOP2015, SAS2015にて発表した。会議の論文採択数・採択率はそれぞれ147本中36本・24%、113本中33本・29%、44本中18本・41%である。また、この研究に関する成果をまとめた招待講演を「3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016)」にて行った。
2.依存型システムによるオブジェクト指向言語プログラムの検証の研究を行った。高階プログラム検証で用いた技術の応用を目指した研究である。成果をまとめたポスター発表を国際会議APLAS 2015にて行った。
3.高階プログラムのための時相論理仕様検証について研究を行い成果を上げた。成果をまとめた論文を国際会議POPL 2016で発表した。会議の論文採択数は252本中59本であり採択率は23%である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究はおおむね順調に進展している。「研究実績の概要」で述べたとおり、述語抽象改良の研究と高階プログラムの検証に関する基盤的研究において実績をあげた。
|
| 今後の研究の推進方策 |
引き続き、述語抽象の改良等、高階言語で記述されたプログラムの検証に関する研究を行う。
|
| 次年度使用額が生じた理由 |
人件費に関して、当初の予定と異なる支出が必要となったため、次年度使用額が生じた。具体的には、研究機関の構成変更(研究科統合)に伴い、他予算(研究科長裁量経費)との折半で支払われる学生の謝金が各年度50%,50%という予定から、今年度0%,次年度100%という内訳になったため。
|
| 次年度使用額の使用計画 |
理由で述べたとおり、生じた差額は人件費(研究に関する実験など研究補助の謝金)として使用する。他は当初の計画通り、国内外の会議での研究調査・成果発表のための旅費および学会参加費、また論文別刷り代・論文掲載料などに使用する。
|
