Specification and Verification of Convergent Replicated Data Types
Convergent Replicated Data Types (CRDTs) are data types which can be replicated across multiple nodes. Operations are performed on only a single replica and updates are communicated to other replicas at some later time. A CRDT guarantees that different replicas converge and eventually are in the same state.
This goal of this thesis is to present an approach to specify the functional behaviour of a CRDT and provide a framework for verifying the behaviour of a CRDT implementation using the interactive theorem prover Isabelle/HOL. The approach has been used to specify and verify some known CRDTs.