2015 Fiscal Year Research-status Report
高階プログラミング言語で記述された大規模ソフトウェアの検証
| Project/Area Number |
26330082
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | ソフトウェア検証 / モデル検査 / 高階関数 / 述語論理 / 抽象詳細化 / 時相論理 |
|---|
| Outline of Annual Research Achievements |
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%である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究はおおむね順調に進展している。「研究実績の概要」で述べたとおり、述語抽象改良の研究と高階プログラムの検証に関する基盤的研究において実績をあげた。
|
| Strategy for Future Research Activity |
引き続き、述語抽象の改良等、高階言語で記述されたプログラムの検証に関する研究を行う。
|
| Causes of Carryover |
人件費に関して、当初の予定と異なる支出が必要となったため、次年度使用額が生じた。具体的には、研究機関の構成変更(研究科統合)に伴い、他予算(研究科長裁量経費)との折半で支払われる学生の謝金が各年度50%,50%という予定から、今年度0%,次年度100%という内訳になったため。
|
| Expenditure Plan for Carryover Budget |
理由で述べたとおり、生じた差額は人件費(研究に関する実験など研究補助の謝金)として使用する。他は当初の計画通り、国内外の会議での研究調査・成果発表のための旅費および学会参加費、また論文別刷り代・論文掲載料などに使用する。
|
Research Products
(8 results)
-
[Journal Article] Temporal Verification of Higher-Order Functional Programs2016
Author(s)
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
-
Journal Title
In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices
Volume: 51 (1)
Pages: 57-68
DOI
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
