16:00-17:30

Guest lecture by Dr. Stephan Merz from INRIA

Dr. Stephan Merz from INRIA will give a talk in the elite program’s special lecture series. The talk will take place as an online meeting.

Title

The TLA+ Language and Tool Set

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.