recent talks
student projects

Stephan Merz — research projects

I have been leading the VeriDis research team of INRIA Nancy since January 2010. VeriDis is intended to be 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 has passed the INRIA evaluation process, and we are waiting for the lawyers to draft an agreement for the project to be officially created.

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.

Our team here at LORIA mostly works on applying refinement concepts to the development of computerized systems. Our group has particular experience with the (Event-)B method and the TLA+ language (see also the community page). MOSEL is also the name of the river that connects the east of France, Luxembourg, and the west of Germany.
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.

Stephan Merz