Markus is a principal research software engineer at Microsoft Research. He has been a member of the TLA+ project for over a decade. In this role, Markus has made significant contributions to the development of the TLA+ tools and has helped engineers at Microsoft formalize their systems using TLA+. Markus also regularly teaches TLA+ to engineers at Microsoft and elsewhere, sharing his knowledge and experience.
TLA+ is a language for the specification and verification of discrete systems, including concurrent and distributed algorithms. The behavior of systems is described in the form of state machines, written in a language based on mathematical set theory and temporal logic. The same language also serves to express safety and liveness properties. TLA+ is supported by tools for computer-assisted verific...