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.
Wed 6 SepDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | Verification 1ICFP Papers and Events at A - Grand Ballroom 2 Chair(s): Tahina Ramananandro Microsoft Research | ||
10:30 30mTalk | Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification ICFP Papers and Events DOI | ||
11:00 30mTalk | Higher-Order Property-Directed Reachability ICFP Papers and Events Hiroyuki Katsura University of Tokyo, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo DOI | ||
11:30 30mTalk | Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation ProtocolsRemote ICFP Papers and Events Léon Gondelman Aarhus University, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, Amin Timany Aarhus University, Lars Birkedal Aarhus University DOI | ||