QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
summary
QuickSilver introduces the Mercury modeling language with two concrete agreement primitives, Partition and Consensus, that abstract verified Paxos/Raft-style protocols. It proves decidability for systems that are phase-compatible with permissible safety properties by reducing to a MercuryCore decidable fragment, then computes small cutoffs (all benchmarks use ≤5 processes) to reduce parameterized checking to finite model checking. The tool fully automates verification for case studies (data store, lock service, robotics, ledger) and completes the largest example in under 12 minutes.
AI-written summary · about
chapters (10)
- 0:00Start
- 2:55Quicksilver Framework for Modeling
- 3:34Modeling Language
- 4:42Consensus
- 9:42Local Semantics of a Mercury Program
- 11:10Local Semantics
- 12:08Transitions
- 12:56Evaluation Results
- 13:48Robotics Motion Planning
- 14:13Conclusion
related talks
21mEnabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
20mModel Checking Distributed Protocols in Must
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
13mSharding the State Machine: Automated Modular Reasoning for Complex Concurrent System
25mProperty-agnostic base case extension for scalable verification of distributed systems
38mThe Verification of a Distributed System
54mReduction theorems for effective parameterized verification of round- based distributed algorithms