Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
summary
Claims that propositional PDR is an instance of abstract interpretation by defining Lambda-PDR (take all counterexample generalizations) and a logical abstract domain called the monotone span. Shows frames are Kleene iterations of the best abstract transformer in that domain, and proves concrete consequences: simple binary-counter example converges in two frames under Lambda-PDR while exact forward reachability needs exponentially many, demonstrating an exponential gap. Provides syntactic convergence bounds (single-cube bk, product bounds for multiple cubes) and notes Lambda-PDR is theoretical, not yet efficient.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:27Invariant Inference
- 2:08IC3PDR
- 3:36The usual explanation
- 6:53PDL Frames
- 9:03Significant Over Approximation
- 10:23The Monotone Span
- 11:53The Best Abstract Transformer
- 14:27Geometric Interpretation
- 15:50Convergence bounds
- 16:41Upper bounds
- 17:13Example
- 19:20Proof
- 20:09Conclusion
related talks
28mHigher-Order Property-Directed Reachability
24mThe Best of Abstract Interpretations
21mRelating Distances and Abstractions: An Abstract Interpretation Perspective
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
18mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
23mAn Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
19mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…)
36mParallel Algebraic Effect Handlers