© 2021 Strange Loop
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 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.