研究課題
本研究では、研究代表者がこれまでに研究・開発を行ってきた高レベル言語のための検証理論であるリファインメント型システムおよびホーン節制約解消法、関数型言語 OCaml のための全自動・高精度検証ツールである RCaml を発展させ、実用上重要であるにも関わらず既存手法では十分に扱えなかった言語機能（再帰データ構造・参照セル・オブジェクト・モジュール機構・例外処理機構・マルチスレッド機構）および仕様（時相的仕様・関係的仕様）の全自動・高精度検証法の確立を目指した。今年度は、依存リファインメント型システムの型推論問題や時相的・関係的仕様検証問題から帰着される不動点論理式の妥当性判定問題を自動的に解消するためのソルバーであるMuValおよびMu2CHCの研究・開発を行った。MuValおよびMu2CHCはそれぞれ、不動点論理式の妥当性判定問題をpCSPおよびCHCというクラスの述語制約解消問題に帰着して解くものである。さらに、pCSPの制約解消を、不変条件・ランキング関数・スコーレム関数を自動合成することによって行うソルバーPCSatの研究・開発も行った。これらの成果を4報の論文にまとめた。そのうちPCSatに関する論文1報はAI分野のトップ会議であるAAAI20に、Mu2CHCに関する論文はプログラム解析の主要会議SAS19にそれぞれ採録され、発表を行った。
令和元年度が最終年度であるため、記入しない。
すべて 2020 2019
すべて 雑誌論文 (2件) (うち査読あり 2件、 オープンアクセス 1件) 学会発表 (2件) (うち国際学会 2件)
Proceedings of the annual AAAI Conference on Artificial Intelligence (AAAI 2020)
巻: 印刷中 ページ: 印刷中
Proceedings of the 26th International Static Analysis Symposium (SAS 2019)
巻: LNCS 11822 ページ: 413～436
10.1007/978-3-030-32304-2_20
