TLA+ is a language for the specification and verification of discrete systems, including concurrent and distributed algorithms. The behavior of systems is described in the form of state machines, written in a language based on mathematical set theory and temporal logic. The same language also serves to express safety and liveness properties. TLA+ is supported by tools for computer-assisted verification, including model checkers for verifying finite instances and an interactive proof system. In summary, TLA+ is a design tool to build reliable systems that don't need patching at 3 am on weekends.
In this talk, we will take the hands-on approach and study the powers of TLA+ by collectively solving a subtle concurrency issue that (as we will pretend) has brought our system down even though the system was heavily tested.
Markus is a principal research software engineer at Microsoft Research. He has been a member of the TLA+ project for over a decade. In this role, Markus has made significant contributions to the development of the TLA+ tools and has helped engineers at Microsoft formalize their systems using TLA+. Markus also regularly teaches TLA+ to engineers at Microsoft and elsewhere, sharing his knowledge and...