Specification and Verification of Convergent Replicated Data Types
Conflict Free Replicated Data Types (CRDTs) can be used as basic building blocks for storing and managing data in a distributed system. They provide high availability and performance, and they guarantee that conflicts are resolved in a well defined way. In this master's thesis, techniques for verifying these data types with the interactive theorem prover Isabelle/HOL are presented. The verification covers convergence properties, as well as behavioral specifications. For this task, a basic framework for the verification of CRDTs has been developed and several known CRDTs from the literature have been verified using the framework. The result are machine checked proofs for the correctness of the CRDTs, which rely on only a small set of unchecked assumptions, which are captured in a simple system model.