Markus A. Kuppe, Microsoft
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 A. Kuppe, Microsoft
Markus Kuppe is a Principal Research Software Development Engineer at Microsoft Research in Redmond, WA. As an engineer, his focus is on making spec-driven development (with TLA+) more popular among fellow engineers: This includes scaling verification to larger, real-world problems, and building tools to combine spec-driven development with established software engineering processes.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
author = {Markus A. Kuppe},
title = {Weeks of Debugging Can Save You Hours of {TLA+}},
booktitle = {SREcon20 Americas (SREcon20 Americas)},
year = {2020},
url = {https://www.usenix.org/conference/srecon20americas/presentation/kuppe},
publisher = {USENIX Association},
month = dec
}