During his PhD studies, Abel researched the formal verification of Conflict-free Replicated Data Types (CRDTs), a family of distributed data structures. CRDTs can be used in decentralized distributed systems to increase availability in the face of network partitions or limited connectivity. They have applications in storage of data as well as collaborative text editing, and have gained in popularity in recent years with the adoption of cloud computing. Abel used Aneris, a separation logic for reasoning about distributed systems, to develop a unified approach to the specification and verification of CRDTs. 

The new research findings show how we can formally reason about CRDTs in an abstract and modular way, without revealing internal implementation details. They contribute to our understanding of how to develop secure, error-free software.

The PhD study was completed at the Logic and Semantics Group (LogSem), Faculty of Natural Sciences, Aarhus University.
This summary was prepared by the PhD student.

Time: Thursday September 28 , at 13:00
Place: Building 5342, room 333, Ada, Institut for Datalogi, Åbogade 34, 8200 Aarhus N, Danmark
Title of PhD thesis: Conflict-free Replicated Data Types have Abstract Data Types
Contact information: Abel Nieto, e-mail: abeln@cs.au.dk 

Members of the assessment committee:
Professor Ilya Sergey, Associate Professor, National University of Singapore, Singapore 
Professor Jesper Bengtson, Associate Professor, IT-University of Coppenhagen, Denmark
Professor Susanne Bødker (chair), Institut for Datalogi, Aarhus University, Denmark

Main supervisor:
Lars Birkedal, LogSem, Aarhus University, Denmark

Co-supervisor:
 Amin Timany, LogSem, Aarhus University, Denmark 

Language: The PhD dissertation will be defended in English

The defence is public.
The PhD thesis is available for reading at the Graduate School of Natural Sciences/GSNS,
Jens Baggesens Vej 53, building 5221, 8200 Aarhus N.