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}
}