Verifying Almost-Sure Termination for Randomized Distributed Algorithms
summary
Presents a sound proof rule that combines martingale-based arguments with reasoning about weak fairness and produces SMT-based proofs for almost-sure termination of randomized distributed algorithms. Implements the rules on top of Caesar and verifies parametrized consensus protocols including Ben-Or's protocol and graded binary consensus under crash and Byzantine faults. Handles unbounded state and unbounded variant functions, produces certificates (probabilistic variants plus supermartingales) and reports machine-checked proofs; some supermartingales use exponentials beyond template-based reach.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:24Consensus as fundamental problem
- 6:15Ben-Or’s consensus algorithm
- 11:14Proof rules for termination
- 16:55Fairness-aware termination rule
- 19:26Machine-checked consensus proofs
- 20:11Future work
- 20:32Q&A
related talks
18mSureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…)
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
45mCorrectness proofs of distributed systems with Isabelle
48mThe Verification of a Distributed System
25mProperty-agnostic base case extension for scalable verification of distributed systems
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
42mStochastic reasoning in decentralised systems
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...