Introduction to TLA+ (Annette Bieniusa)
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+.
This session is held on in Tutorials A