Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...
summary
Presents Venus, an implementation that extends Quicksilver to verify systems that are unbounded in both process count and data by reducing variable domains via value symmetry and a new bounded region notion. Uses componentwise permutations on Mercury DSL models to collapse unbounded payloads while preserving critical equalities, shows consensus cardinality 1 and a finite region suffice, and reports a domain-of-size-3 reduction. Verifies a consortium-arbitration model, an atomic register, and a Redis-like key value store.
AI-written summary · about
chapters (10)
- 0:00Bounded verification intro
- 1:48Unbounded verification challenges
- 3:53Quicksilver limitations
- 4:55Consortium protocol example
- 8:02Venus unbounded domains
- 11:11Value symmetry in verification
- 14:40Venus case studies
- 15:42Q&A: Venus vs TLA+ vs T+
- 17:52Q&A: Why not T+ directly
- 19:17Q&A: Message passing model
related talks
15mQuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
25mSafe Replication through Bounded Concurrency Verification
48mThe Verification of a Distributed System
25mProperty-agnostic base case extension for scalable verification of distributed systems
18mSureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…)
38mThe Verification of a Distributed System