Weeks of Debugging Can Save You Hours of TLA+

Due to the evolving Coronavirus/COVID-19 situation, SREcon20 Americas West has been rescheduled to June 2–4, 2020.
More information is available here.

Wednesday, March 25, 2020 - 12:20 pm1:00 pm

Markus A Kuppe, Microsoft Research


Designing and debugging a concurrent program or distributed system is hard and time-consuming. It is the proverbial search for the needle in the ever changing haystack. Wouldn't it be cool if we could explore the actual algorithm hidden inside of the implementation and check that its correctness even before we write a single line of the implementation code?

It turns out we can: The TLA+ specification language is an immensely expressive language that enables rapid prototyping of ideas. It has once been coined "debuggable pseudo-code". And TLA+ comes with a set of tools with which users can verify correctness properties.

In this talk, we will study the powers of TLA+ by solving challenge Fourteen of the famous c2 wiki in 40 minutes.

Markus A Kuppe, Microsoft Research

Markus Kuppe is a Principal Research Software Development Engineer at Microsoft Research. He joined the TLA+ project in 2011. Being an engineer, his focus is on making spec-driven development (with TLA+) more popular among fellow engineers.

@conference {247283,
author = {Markus A Kuppe},
title = {Weeks of Debugging Can Save You Hours of TLA+},
year = {2020},
address = {Santa Clara, CA},
publisher = {{USENIX} Association},
month = mar,