Towards a Theoretical Understanding of Property-Directed Reachability

on YouTube ↗59m

" summary

Shows that the SAT queries used by property‑directed reachability are strictly stronger than plain inductiveness checks, proving IC3 cannot be implemented in the ICE framework and exhibiting an exponential separation: a class of transition systems admits a polynomial‑query PDR‑style algorithm while any inductiveness‑query learner needs exponentially many queries. Defines an eager variant, Lambda‑PDR frames = monotone abstract interpretation, and proves PDR’s frames can exponentially overapproximate exact forward reachability.

AI-written summary · about

" chapters (15)

1. 0:00Intro
2. 1:21Safety of Transition Systems
3. 2:31Inductive Invariants
4. 6:38Lemmas Block Counterexamples
5. 9:45Exact Concept Learning with Equivalence & Membership Queries
6. 11:23SAT-Based Invariant Inference as Inference with Queries
7. 13:01Inductiveness-Query Model
8. 16:25Hoare-Query Model
9. 24:17Part II: PDR's Generalization
10. 34:58b-Monotone Formulas
11. 40:29Monotone Span Abstract Domain
12. 42:24Abstract Interpretation in MSpan
13. 42:54Best Abstract Transformer
14. 45:06Abstraction & Monotone Theory
15. 50:26Summary