2019 Fiscal Year Annual Research Report
Temporal and Relational Verification of High-Level Programs
| Project/Area Number |
16H05856
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | 依存リファインメント型 / 時相的・関係的仕様 / 述語制約解消 / 不動点論理 / 不変条件 / ランキング関数 / スコーレム関数 |
|---|
| Outline of Annual Research Achievements |
本研究では、研究代表者がこれまでに研究・開発を行ってきた高レベル言語のための検証理論であるリファインメント型システムおよびホーン節制約解消法、関数型言語 OCaml のための全自動・高精度検証ツールである RCaml を発展させ、実用上重要であるにも関わらず既存手法では十分に扱えなかった言語機能（再帰データ構造・参照セル・オブジェクト・モジュール機構・例外処理機構・マルチスレッド機構）および仕様（時相的仕様・関係的仕様）の全自動・高精度検証法の確立を目指した。
今年度は、依存リファインメント型システムの型推論問題や時相的・関係的仕様検証問題から帰着される不動点論理式の妥当性判定問題を自動的に解消するためのソルバーであるMuValおよびMu2CHCの研究・開発を行った。MuValおよびMu2CHCはそれぞれ、不動点論理式の妥当性判定問題をpCSPおよびCHCというクラスの述語制約解消問題に帰着して解くものである。さらに、pCSPの制約解消を、不変条件・ランキング関数・スコーレム関数を自動合成することによって行うソルバーPCSatの研究・開発も行った。
これらの成果を4報の論文にまとめた。そのうちPCSatに関する論文1報はAI分野のトップ会議であるAAAI20に、Mu2CHCに関する論文はプログラム解析の主要会議SAS19にそれぞれ採録され、発表を行った。
|
| Research Progress Status |
令和元年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和元年度が最終年度であるため、記入しない。
|
