Annette Bieniusa

Senior researcher at TU Kaiserslautern

Annette is a lecturer and senior researcher at the Technische Universität Kaiserslautern. Her research interests include semantics of concurrent and distributed programming, with a focus on replication, synchronization, and how they are reflected on a programming language level. Annette was involved in several national and international research projects, most recently in the EU-Projects “SyncFree: Large-scale Computation without Synchronization” and “Lightkone: Lightweight computation for networks at the edge“. She is also leading the development of AntidoteDB, a transactional CRDT-key value store.

Past Activities

Annette Bieniusa
Code Mesh V
Tutorial/ 05 Nov 2020
16.00 - 19.30

Introduction to TLA+

Concurrent and distributed programs are notoriously difficult to get right. Even tiny variations of algorithms like Peterson’s lock for mutual exclusion lead to significantly different behaviours and errors that are complex to locate.

TLA+ is a high-level language for modelling such programs and specifying their behaviour in a rigorous way. In this tutorial, you will learn how to write concurrent and distributed algorithms in PlusCal, a pseudo-code like interface for TLA+, and how to specify correctness conditions using temporal logic. We will further apply the model-checker TLC and discuss typical pitfalls when working with TLA+.



Level required to take the course 



2h 30 minutes



Please install the TLA Toolbox on your machine by following the instructions on this page.

Annette Bieniusa / Nuno Preguiça
Code Mesh LDN 2018
Tutorial/ 07 Nov 2018
13.30 - 17.00

Just the right kind of Consistency!

13:30 - 17:00

You need a data store that allows for high throughput and availability, but you are worried about the consistency of your data under concurrent updates when replicating across data centers? Current designs for data storage forces application developers to decide early in the design cycle, and once and for all, what type of consistency the database should provide.

At one extreme, data stores with strong consistency (such as Spanner and CockroachDB) require frequent global coordination; restricting concurrency in this way greatly simplifies application development, but it reduces availability and increases latency.

At the opposite extreme, there are systems like Cassandra that provide eventual consistency only: they never sacrifice availability, but application developers must write code to deal with all sorts of concurrency anomalies in order to prevent violation of application invariants. But the system just needs to be consistent enough for the application to be correct!

In the training day, we will review different approaches and tools for choosing just the right kind of consistency for your app.


You will learn how conflict-free replicated datatypes (CRDTs), transactions, and causal consistency interact to keep your data safe. Further, you will see how to analyse your application and its invariants to obtain a provable correct model. This tutorial is hands-on with many interactive elements to explore the features and limits of the Just-Right Consistency approach.


Application developers and system developers.

Annette Bieniusa
Code BEAM Lite Munich 2018
07 Dec 2018
14.45 - 15.25

AntidoteDB: a planet scale, highly available, transactional database

Cloud-scale applications must be highly available and offer low latency responses while serving an ever-growing number of users concurrently.
To achieve these goals, these apps rely on distributed cloud data stores that provide availability even under network partition.
It takes significant effort and expertise from programmers to understand the intricate semantics and develop correct applications on top of such highly available databases. 
In my talk, I will show how AntidoteDB supports a principled approach to build highly-available, yet correct applications by combining conflict-free replicated data types (CRDTs), highly-available transactions and stronger synchronisation mechanisms.


You will learn how conflict-free replicated datatypes (CRDTs), transactions, and causal consistency interact to keep application data safe. Further, you will see how to identify patterns in your application that have specific synchronisation requirements und learn how to employ them with AntidoteDB.


App developers that rely on datastores