Induction Duality: Primal-Dual Search for Invariants
summary
Presents a formal induction duality linking execution traces and bounded incremental proofs, and derives primal-dual Houdini, a symmetric algorithm that alternates discovering states and predicates. Proves termination for either k‑provable properties or unsafe systems and shows every iteration can add a useful state or predicate. Implements a k=1 prototype for distributed protocol verification, compares with IC3-style tools, and empirically handles several difficult benchmarks—uniquely solving some and matching others, but failing where k must be larger.
AI-written summary · about
chapters (10)
- 0:00Problem: Invariant inference
- 0:34Contributions
- 1:22Execution vs Incremental Induction
- 4:18Formalizing symmetric incremental induction
- 5:22Executions vs Incremental Induction: Symmetry
- 7:50Induction Duality Structure
- 11:09Houdini and Dual Houdini
- 13:59Primal-Dual Houdini: Theorems
- 15:47Evaluation for Distributed Protocols (k = 1)
- 19:26Conclusion