Mostly Automated Verification of Liveness Properties for Distributed Protocols w...
summary
LVR reduces liveness to a set of safety checks plus a termination proof: synthesize a nonnegative integer ranking function that strictly decreases on every transition, check no-deadlock and no-give-up as safety properties, then use an off‑the‑shelf invariant prover (pf3) for the safety proofs. Ranking functions are linear polynomials over mutable integer variables; a static analyzer extracts variable bounds and deltas, passes coefficient constraints to an SMT solver (coefficient solving <1s), and completes full proofs for Paxos variants and other protocols in hours with only a few user hints.
AI-written summary · about
chapters (11)
- 0:00Automated liveness verification
- 1:44Ticket lock protocol
- 3:30Challenges in liveness
- 4:58LVR method overview
- 7:29Liveness to safety reduction
- 8:54Ranking functions for protocols
- 10:18Linear polynomial constraints
- 12:04Static analysis for delta
- 13:28Experimental results
- 14:30Conclusion
- 14:51Q&A
related talks
28mLiveness to Safety for Distributed Systems
17mLiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
38mThe Verification of a Distributed System
25mProperty-agnostic base case extension for scalable verification of distributed systems
48mThe Verification of a Distributed System
17mAnvil: Verifying Liveness of Cluster Management Controllers
26mScaling Up Livelock Verification for Network-on-Chip Routing Algorithms
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms