Stephan Merz — research projects

VeriDis

I have been leading the VeriDis research group of INRIA Nancy since January 2010. VeriDis is a joint project with the Automation of Logic Group, led by Christoph Weidenbach, of Max-Planck Institut für Informatik in Saarbrücken, Germany. In June 2011, the proposal passed the INRIA evaluation process, and VeriDis was officially created in July, 2012.

The scientific objectives of VeriDis are to combine methods, tools, and techniques for the verification of distributed algorithms and systems. In particular, the teams in Nancy and Saarbrücken are developing the VeriT SMT solver and the Spass theorem prover.

TLA+ Proof System and TLA Toolbox

Much of my work is related to the theory and applications of Leslie Lamport's Temporal Logic of Actions and the specification language TLA+ (see also my publication page).

I am a member of the project Tools and Methodologies for Formal Specifications at the Joint Centre of INRIA and Microsoft Research in Saclay, close to Paris. This project funds much of the development of TLAPS, the TLA+ Proof System.

Some supplementary material on the design of TLAPS and its back-end provers is available here.

Our largest case study so far on the use of TLAPS, carried out as part of two PhD projects, concerns the formal verification of a variant of the Pastry algorithm, and is documented here.