Model Checking Distributed Protocols in Must
summary
Must is a bounded model checker that verifies real distributed implementations by instrumenting a mainstream language (example: Rust) with a tiny concurrency API of three ops: nondeterministic choice, send, receive. It uses a novel dynamic partial order reduction that is sound, complete, optimal, parametric over communication models, and uses polynomial memory. Semantics build and enumerate partial-order graphs; features include non‑blocking and selective receives and monitors for global properties, and it scales to verify systems like replicated logs and distributed transactions.
AI-written summary · about
chapters (7)
- 0:00Formal methods in distributed systems
- 1:23Must design principles
- 3:10Declarative semantics and reduction
- 6:48Non-blocking and selective receives
- 11:29System-wide properties with monitors
- 13:59Must practicality and case studies
- 15:02Q&A
related talks
13mTesting LLM-Generated Distributed Protocol Code
15mQuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
20mImplementability of Global Distributed Protocols Modulo Network Architectures
38mThe Verification of a Distributed System
45mCorrectness proofs of distributed systems with Isabelle
16mModel Checking for a Multi-Execution Memory Model
48mThe Verification of a Distributed System
21mEnabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...