Higher-Order Property-Directed Reachability
summary
Formalizes a higher-order extension of PDR that extends PDR to nu-HFL(Z) so transition systems can be described by higher-order recursive functions, implements a prototype HoPDR solver using polymorphic refinement and intersection types, and evaluates it on higher-order safety benchmarks. Results show it does not yet beat all existing solvers but solves some unsafe cases Leso cannot and a combined HoPDR+Leso solver is the best; the prototype is promising but needs engineering for faster fixpoint solving.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:06Motivation for program verification
- 3:15Targeting new HFL
- 6:26Property-Directed Reachability
- 8:57Extending PDR to higher-order
- 10:00Refinement type system
- 12:30Formalizing Higher-Order PDR
- 16:25Running example
- 21:03Experimental results
- 22:28Related work
- 23:32Conclusion
- 24:34Q&A
related talks
26mProperty-Directed Reachability as Abstract Interpretation in the Monotone Theory
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
19mHOL4P4: mechanized small-step semantics for P4
14mHigher-order Automation In TLAPS
14mOn Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
23mHigher-Order MSL Horn Constraints
14mHigher-Order Demand-Driven Symbolic Evaluation
15mFaster Reachability Analysis for LR(1) Parsers