研究課題
前年度に引き続き、再帰データ構造と再帰関数を含むプログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階不動点論理(first-order fixpoint logic)に関する研究を行った。特に、前年度に開発した、constrained Horn clauses(CHCs)を拡張した述語制約クラスpfwCSPの制約解消問題に一階述語不動点論理の定理証明問題を帰着し、制約解消アルゴリズムにより自動定理証明を実現するアルゴリズムを、一階不動点論理が持つ双対性を利用することで、入力の問題とその否定をそれぞれの部分解から得られる情報を交換することにより高速に同時並行に解く手法についての研究を行った。加えて、pfwCSPの制約解消を直接使うことにより、複雑な関係性仕様の検証を行う手法についての研究を行った。具体的には、pfwCSPの制約をうまく使うことにより、無限状態命令型プログラムに対して、非同期的なself compositionが必要な性質や、co-terminationやgeneralied non-interferenceといったhypersafetyでない関係性仕様の検証を行う手法を提案した。これらの研究の成果をまとめた論文はプログラム検証分野の最高峰の国際会議であるInternational Conference on Computer-Aided Verificationに採録された。加えて、型エフェクトシステムによる代数的エフェクトハンドラ(algebraic effects and handlers)を含むプログラムに対する時相論理仕様の検証についての研究を行った。
令和3年度が最終年度であるため、記入しない。
すべて 2022 2021
すべて 雑誌論文 (1件) (うち国際共著 1件、 査読あり 1件、 オープンアクセス 1件) 学会発表 (3件) (うち国際学会 1件、 招待講演 1件)
In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science
巻: 12759 ページ: 742～766
10.1007/978-3-030-81685-8_35
