2021 Fiscal Year Annual Research Report
Verification of high-level programs containing mutable higher-order recursive data structures
| Project/Area Number |
17H01720
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Keywords | プログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 分離論理 / 循環証明 / 代数的エフェクト |
|---|
| Outline of Annual Research Achievements |
前年度に引き続き、再帰データ構造と再帰関数を含むプログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階不動点論理(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)を含むプログラムに対する時相論理仕様の検証についての研究を行った。
|
| Research Progress Status |
令和3年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和3年度が最終年度であるため、記入しない。
|
-
[Journal Article] Constraint-Based Relational Verification2021
Author(s)
Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
-
Journal Title
In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science
Volume: 12759
Pages: 742～766
DOI
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
