Property-agnostic base case extension for scalable verification of distributed systems
summary
Verifies that LTL properties checked on a tiny MyCHIP cycle (one originator, one relay, one referee) extend to any-size ring by combining a Spin model checker base case with an inductive conformance proof based on Dill’s trace theory and a Coq-style interactive proof. Four properties are verified on the base: termination, global commit agreement, bounded balance harm, and active-pair agreement (16,000 states, 172,000 edges, 10.5s). The mechanized proof is ~24 lemmas, ~2,000 LOC, 8s to check; nine trace equivalence classes use model checking (28s) to close the gap.
AI-written summary · about
chapters (10)
- 0:00Scalable verification methods
- 2:02myCHIPs system case study
- 7:21Model checking and theorem proving
- 9:07Base case verification
- 11:13Inductive proof structure
- 12:59Verifying system properties
- 14:02Conformance equivalence
- 17:40Safe substitution
- 21:14Inductive proof results
- 22:41Q&A
related talks
38mThe Verification of a Distributed System
48mThe Verification of a Distributed System
45mCorrectness proofs of distributed systems with Isabelle
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
28mReasoning about Distributed Reconfigurable Systems
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
14mBolt-On Strong Consistency: Specification, Implementation, and Verification