Event Details

Speaker: Dr Stephan Merz

Talk: Specifying and verifying algorithms in TLA+

Date: June 10th, 2022

Time: 14:00-15:00

Teams Link: Join Seminar (We’d appreciate if you could optionally register to join our mailing list)

Abstract:

TLA+ is a formal language, based on mathematical set theory and temporal logic, for describing algorithms, and it is supported by explicit-state and symbolic model checkers, as well as an interactive proof assistant, for verifying their properties. Using distributed termination detection as a running example, this talk will introduce the fundamental concepts of TLA+ and also give an overview of the TLA+ toolset.

Biography:

Stephan Merz received his PhD from the University of Munich in Germany. Since 2002 he has been a senior researcher at Inria, where he heads the VeriDis research group. His research interests are centered on formal methods for the description and verification of algorithms and systems, including model checking and theorem proving. He contributes to the TLA+ Proof System, a proof assistant for reasoning about TLA+ specifications.

Please contact Jennifer for any Teams connectivity issues: j.mcculloch@lancaster.ac.uk