Strange Loop

2009 - 2023

/

St. Louis, MO

TLA-plus Workshop

This workshop will show developers of concurrent and distributed systems how to model algorithms with TLA+. Its focus is on applying TLA+ rather than the TLA+ language itself. In other words, the workshop will follow Lamport's video course style and introduce TLA+ as we go. At the end of the day, you will have written a specification of a termination detection algorithm (EWD998), checked safety and liveness properties, stated fairness constraints, and encountered refinement. This workshop is a fast-paced, hands-on simulation of real-world spec writing. A detailed agenda is at https://github.com/lemmy/ewd998/issues/3. The workshop material is made available at https://github.com/lemmy/ewd998.

Markus Kuppe

Markus Kuppe

Microsoft Research

Markus Kuppe is a principal research software engineer at Microsoft Research. He has been part of the TLA+ core team for a decade and is one of the organizers of TLA+ pre-conf.