一句话：提出 PDR 的高阶扩展 HoPDR，用于高阶递归函数描述的系统及高阶程序安全性质验证。
本文提出性质导向可达性（PDR）的高阶扩展 HoPDR，用于以高阶递归函数描述迁移系统时的自动验证。作者将 HoPDR 形式化为带整数与最大不动点算子的合取式高阶不动点逻辑 nu-HFL(Z) 的有效性检查问题；该问题也可看作约束 Horn 子句（CHC）可满足性判定问题的高阶扩展，高阶程序的安全性质验证可自然归约到它。作者实现了基于 HoPDR 的原型验证工具，实验确认其有效性，并与一阶系统的 PDR 及已有全自动高阶程序验证方法进行比较。
The property-directed reachability (PDR) has been used as a successful method for automated verification of first-order transition systems. We propose a higher-order extension of PDR, called HoPDR, where higher-order recursive functions may be used to describe transition systems. We formalize HoPDR for the validity checking problem for conjunctive nu-HFL(Z), a higher-order fixpoint logic with integers and greatest fixpoint operators. The validity checking problem can also be viewed as a higher-order extension of the satisfiability problem for Constrained Horn Clauses (CHC), and safety property verification of higher-order programs can naturally be reduced to the validity checking problem. We have implemented a prototype verification tool based on HoPDR and confirmed its effectiveness. We also compare our HoPDR procedure with the PDR procedure for first-order systems and previous methods for fully automated higher-order program verification.
@article{paperbot1916,
title = {Higher-Order Property-Directed Reachability},
author = {Hiroyuki Katsura and Naoki Kobayashi and Ryosuke Sato},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607831}
}