Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms
summary
Claims an automated verifier that uses a separation logic augmented with message histories and a goal-directed abstract interpretation to soundly over-approximate cyclic message traces. Builds a prototype for the P modeling language that summarizes unbounded voter sets as summary processes and parameterizes cycles by a configuration variable φ, solved via recurrence analysis. Demonstrates automatic safety proofs for a oneshot leader election and reports application to Paxos (first automated Paxos safety proof without user invariants).
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:25Problem statement
- 3:52Execution histories
- 4:33Goal-directed analysis
- 5:55Unsafe states in leader election
- 8:46Parameterizing histories
- 10:32Summary states
- 13:01Tool implementation
- 14:24Limitations and future work
- 15:27Q&A
related talks
17mMessage Chains for Distributed System Verification
25mProperty-agnostic base case extension for scalable verification of distributed systems
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
21mMechanizing the CMP Abstraction for Parameterized Verification
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
28mReasoning about Distributed Reconfigurable Systems
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
15mProducts of Recursive Programs for Hypersafety Verification