Dr. Stephan Merz from INRIA will give a talk in the elite program’s special lecture series. The title of the talk is “The TLA+ Language and Tool Set” and it will take place virtually as an online meeting at 4PM on January 14th 2021.

Abstract

TLA+ is a formal specification language whose foundations are mathematical set theory and temporal logic, and in which systems are described as state machines. It has been adopted mainly by companies that need to design and analyze fault-tolerant distributed and cloud systems. Using classical algorithms for distributed termination detection as a case study, this talk will present the TLA+ language and its tool support in the form of model checking and theorem proving for verifying correctness properties and checking refinement.