Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica
summary
A methodology that links compositional refinement to separation-logic code verification and is fully formalized in Isabelle/HOL, yielding end-to-end trace guarantees for running distributed systems. It translates event-system component models into separation-logic I/O specifications using I/O permissions/tokens, proves trace equivalence between event systems, process calculi, and I/O specs, and checks implementations (Java and Python) with off-the-shelf verifiers (Nagini and VeriFast). Evaluated on three case studies (leader election, primary-backup, entity authentication) and supports UDP/TCP, local concurrency, and multi-language components.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:16Motivation
- 1:40Overview of Igloo Methodology
- 2:52Contributions
- 4:10Leader Election Case Study Steps 1 & 2: Abstract and Protocol Models
- 5:33Refine Into Interface Model
- 6:53Decomposition
- 7:381/0 Specifications
- 9:04Step 5: I/O Specifications (Case Study)
- 10:10Code Verification
- 11:09Overview of Case Studies
- 11:59From Models to VO Specifications
- 13:00Overall Soundness Guarantee
- 14:25Conclusions and Future Work
related talks
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
15mModular Verification of Op-Based CRDTs in Separation Logic
28mReasoning about Distributed Reconfigurable Systems
14mA Refinement Methodology for Distributed Programs in Rust
18mDistributed Causal Memory for Higher-Order Distributed Separation Logic
15mTLC: Temporal Logic of Distributed Components
45mCorrectness proofs of distributed systems with Isabelle