Details
Speaker: Markus Alexander Kuppe, Twitter: @lemmster
TLA+ is among the most popular specification languages to design and
verify concurrent and distributed algorithms. It is well suited for
these tasks because of its expressive language, which also unifies a
system's description and correctness properties; they are the same. Yet,
the language manual does not require a 700+ page compendium.
In this talk, we will take the hands-on approach and study the powers of
TLA+ by collectively solving a subtle concurrency issue known as
challenge 14 in the extreme programming community--no slides, just
pieces of code, and TLA+ specs, which you can already find at
https://github.com/lemmy/BlockingQueue
Markus Kuppe is a Principal Research Software Development Engineer at
Microsoft Research. He has been part of the TLA+ project for more than a
decade, contributing to all aspects of TLA+.
TLA+