Correct and Conflict-free
PhD defence, Thursday 28 September 2023, Abel Nieto Rodriguez
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: firstname.lastname@example.org
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
Lars Birkedal, LogSem, Aarhus University, Denmark
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.