From the abstract: "In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthes

From the abstract: "In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations."