2014 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. 高階関数型言語で記述されたプログラムに対して有効な「二項到達可能性解析」への帰着による、健全かつ相対的完全な停止性検証の手法を提案した。二項到達可能性解析は命令型言語で記述されたプログラムの停止性検証のため提案された枠組みであり、本研究では、世界で初めてこの枠組みを高階言語に拡張することに成功した。また、この研究をまとめた論文「Automatic Termination Verification for Higher-Order Functional Programs」を国際会議「23rd European Symposium on Programming (ESOP 2014)」にて発表した。会議の論文採択数は109本中27本で、採択率は25%である。
2. 線形時相論理仕様検証に対して有効な「構成的」な検証の枠組みを提案した。線形時相論理仕様は、「いずれXが起こる」などの活性仕様などが記述でき、リアクティブシステムの検証に役立つ。プログラム検証において、構成的な枠組みとは、プログラム項の部分ごとに検証を行い結果を組み合わせることにより全体の検証を可能とする枠組みである。提案手法は依存型およびエフェクトシステムに基づいており、特に高レベル言語で記述されたプログラムの検証に有効である。また、この研究をまとめた論文「Local Temporal Reasoning」を国際会議「Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014)」にて発表した。会議の論文採択数は212本中74本であり、採択率は35%である。
|
| 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 |
出席予定であった国際会議「ETAPS 2015: European Joint Conferences on Theory and Practice of Software」が翌年度に開催されることになったので次年度使用額が生じた。
|
| Expenditure Plan for Carryover Budget |
国内外の会議でのプログラム言語およびプログラム検証に関する研究調査・成果発表のための旅費および会議参加費、プログラム検証実験おいて研究補助の学生を雇用するための謝金、論文別刷代・論文掲載料などに使用する。
|
