Higher-Order Property-Directed Reachability

Explore a groundbreaking extension of property-directed reachability (PDR) for automated verification of higher-order transition systems in this 28-minute conference talk from ICFP 2023. Delve into the proposed Higher-Order Property-Directed Reachability (HoPDR) method, which allows for the use of higher-order recursive functions in describing transition systems. Learn about the formalization of HoPDR for validity checking in conjunctive nu-HFL(Z), a higher-order fixpoint logic with integers and greatest fixpoint operators. Discover how this approach relates to the satisfiability problem for Constrained Horn Clauses (CHC) and its application in safety property verification of higher-order programs. Gain insights into the implementation of a prototype verification tool based on HoPDR and its effectiveness compared to first-order PDR procedures and previous methods for automated higher-order program verification.

[ICFP'23] Higher-Order Property-Directed Reachability