Specification and Verification of Convergent Replicated Data Types

Motivation

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.

Problem/Task description

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.

Supervisor

Dr. Annette Bieniusa