Title: TLA+: The Tools, The Language, and The Application

Speaker: Markus Kuppe    (bio) (bio)

Markus Kuppe is a Principal Research Software Development Engineer in the Research In Software Engineering group at Microsoft Research, Redmond. His focus is on making specification-driven development (with TLA+) more popular among engineers. This includes scaling verification to real-world problems and building tools to combine specification-driven development with established software engineering processes.

When: Tuesday, 14 March 2023 at 1900 hrs (IST)       

Abstract:
TLA+ is a language for formally specifying and verifying discrete systems, including distributed algorithms. Users describe the system as a state machine, written in a language based on mathematical set theory and temporal logic, which also serves to express safety and liveness properties. TLA+ comes with tools for computer-assisted verification, including two model checkers and an interactive proof system. TLA+ is used in academia and industry, e.g., to verify data consistency in cloud applications.

This talk will cover the theory behind TLA+ and how practitioners can write TLA+ specifications with the help of verification tools. Additionally, we will discuss known limitations of the tools and outline current and future research opportunities.