Modular Verification of Op-Based CRDTs in Separation Logic

Explore a 15-minute conference talk from ACM SIGPLAN's OOPSLA that delves into a framework for verifying safety properties of Operation-based Conflict-free Replicated Data Types (op-based CRDTs) using separation logic. Learn about the two-library framework, consisting of a Reliable Causal Broadcast (RCB) protocol and an "OpLib" library, which simplifies the creation and correctness proofs of op-based CRDTs. Discover how this approach allows for implementing new CRDTs as purely-functional data structures without the need to reason about network operations, concurrency control, and mutable state. Gain insights into the implementation of 12 example CRDTs from literature, including replicated registers, sets, CRDT combinators, and use cases of the map combinator. Understand the significance of this technique as the first modular verification approach for op-based CRDTs targeting executable implementations, with proofs conducted in the Aneris distributed separation logic and formalized in Coq.

[OOPSLA] Modular Verification of Op-Based CRDTs in Separation Logic