%0 Conference Proceedings
%T Formal Specification and Verification of CRDTs
%+ University of Kaiserslautern [Kaiserslautern]
%A Zeller, Peter
%A Bieniusa, Annette
%A Poetzsch-Heffter, Arnd
%Z Part 1: Specification Languages and Type Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 34th Formal Techniques for Networked and Distributed Systems (FORTE)
%C Berlin, Germany
%Y Erika Ábrahám
%Y Catuscia Palamidessi
%I Springer
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-8461
%P 33-48
%8 2014-06-03
%D 2014
%R 10.1007/978-3-662-43613-4_3
%K CRDT
%K formal verification
%K eventual consistency
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Convergent Replicated Data Types (CRDTs) can be used as basic building blocks for storing and managing replicated data in a distributed system. They provide high availability and performance, and they guarantee eventual consistency. In this paper, we develop a formal framework for the analysis and verification of CRDTs. We investigate and compare the three currently used specification techniques for CRDTs and formalize them based on an abstract model for managing replicated data in distributed systems. We show how CRDT implementations can be expressed in our framework and present a general strategy for verifying CRDTs. Finally, we report on our experiences in using the framework for the verification of important existing CRDT implementations. The framework and the proofs were developed within the interactive theorem prover Isabelle/HOL.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01398007/document
%2 https://inria.hal.science/hal-01398007/file/978-3-662-43613-4_3_Chapter.pdf
%L hal-01398007
%U https://inria.hal.science/hal-01398007
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-8461