PUBLIC VIVA-VOCE NOTIFICATION
Date and Time: Friday, 22 April 2022, 11:30 am
Venue: CMI Seminar Hall (hybrid mode)
On Effective Verification of Replicated Data Types
Gautham Shenoy R
Chennai Mathematical Institute.
22-04-22

---

Abstract

In this talk, we shall look at formal methods for providing cogent specifications and performing effective verification of replicated data types such as the Conflict-free Replicated Data Types (CRDTs)adhering to weaker notions of consistency. We analyse a particularCRDT known as the Observed-Remove Set (OR-Set) where the conflicts between concurrent add and remove operations are handled in aconflict-free manner, even when updates are presented out of order. We provide an optimized implementation of this datatype. Further, we provide a framework for defining declarative specifications for these data types. We present two methodologies to construct bounded reference implementations of these data types. Weshow how these reference implementations can be used for effective verification of given implementations of replicated datatypes. Finally we turn our attention to the verification of read-writekey-value stores that support multiple consistency criteria.