Safe Replication through Bounded Concurrency Verification
summary
Automatic bounded verification explores executions under an unrestricted consistency model but with a finite concurrency bound and discovers concrete invariant-violating counterexamples, then synthesizes minimal consistency-strengthening repairs for specific operations. The implemented tool Q9 analyzes common benchmarks (TPC-C/TPC-E, RUBiS, etc.), uncovers subtle weak consistency anomalies and produces fixes that eliminate violations; typical counterexamples appear with small bounds (often k=1, some cases up to 50–60) and the largest discovery time is under two minutes.
AI-written summary · about
chapters (4)
related talks
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases
20mAn Automated Scalable RISC-V Cache Coherency Verification Project
38mThe Verification of a Distributed System
21mEnabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...
15mTesting Consensus Implementations using Communication Closure
48mThe Verification of a Distributed System
25mProperty-agnostic base case extension for scalable verification of distributed systems