Researchers

Stephan Merz
LORIA
Presentation

I am a researcher at the Inria Nancy research center, a branch of Inria, the French national research institute for computer science. At INRIA Nancy I have been leading the VeriDis team since January 2010. I am also a member of the MOSEL team at LORIA, the laboratory for computer science and its applications in Nancy.

My scientific interests lie in the area of formal verification, in particular of distributed algorithms and systems. We are working on methods, techniques, and tools, including model checking and theorem proving. Check out the TLA+ Proof System, to which we actively contribute.

Among my administrative duties, I am the delegate for colloquia organized at INRIA Nancy and co-head of the PhD committee for computer science in Nancy. From 2005 to 2011, I was a member of INRIA’s evaluation committee, and from 2008 to 2012, I was a member of Section 7 of the National Committee of Scientific Research (CoNRS). I am the INRIA representative at the Scientific Directorate of Schloss Dagstuhl – Leibniz Center for Informatics.

Before joining INRIA, I worked at the University of Munich, Germany.

Contact:
rf.airol@zrem.nahpets
+33 354 95 84 78
Publications at the Joint Centre:

2019

Conference papers

titre
Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle
auteur
Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry
article
ITP 2019 – 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 – 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02303987/file/LIPIcs-ITP-2019-13.pdf BibTex

2016

Conference papers

titre
Proving Determinacy of the PharOS Real-Time Operating System
auteur
Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
article
Abstract State Machines, Alloy, B, TLA, VDM, and Z – 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322335/file/final.pdf BibTex
titre
Encoding TLA+ into Many-Sorted First-Order Logic
auteur
Stephan Merz, Hernán Vanzetto
article
Abstract State Machines, Alloy, B, TLA, VDM, and Z – 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.54-69, ⟨10.1007/978-3-319-33600-8_3⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322328/file/tla2smt.pdf BibTex
titre
A Rigorous Correctness Proof for Pastry
auteur
Noran Azmy, Stephan Merz, Christoph Weidenbach
article
Abstract State Machines, Alloy, B, TLA, VDM, and Z – 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.86-101, ⟨10.1007/978-3-319-33600-8_5⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322342/file/Main.pdf BibTex

2015

Preprints, Working Papers, …

titre
Encoding TLA+ set theory into many-sorted first-order logic
auteur
Stephan Merz, Hernán Vanzetto
article
2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244627/file/sets2015.pdf BibTex

2014

Conference papers

titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
article
Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. pp.1-16
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244623/file/final.pdf BibTex
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
article
ARQNL 2014 – Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01063512/file/final.pdf BibTex
titre
Refinement Types for TLA+
auteur
Stephan Merz, Hernán Vanzetto
article
NASA Formal Methods – 6th International Symposium, 2014, Houston, Texas, United States. pp.143-157, ⟨10.1007/978-3-319-06200-6_11⟩
Accès au bibtex
BibTex

2012

Conference papers

titre
Harnessing SMT Solvers for TLA+ Proofs
auteur
Stephan Merz, Hernán Vanzetto
article
12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00760579/file/avocs2012.pdf BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
18th International Symposium On Formal Methods – FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00726631/file/final.pdf BibTex
titre
Formal Verification Of Pastry Using TLA+
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00768812/file/paper.pdf BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p
Accès au bibtex
BibTex
titre
Automatic Verification Of TLA+ Proof Obligations With SMT Solvers
auteur
Stephan Merz, Hernán Vanzetto
article
18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. pp.289-303, ⟨10.1007/978-3-642-28717-6_23⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00760570/file/tla2smt.pdf BibTex

2011

Conference papers

titre
Towards certification of TLA+ proof obligations with SMT solvers
auteur
Stephan Merz, Hernán Vanzetto
article
First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wroclaw, Poland
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00645458/file/tla2smt.pdf BibTex
titre
Towards Verification of the Pastry Protocol using TLA+
auteur
Stephan Merz, Tianxiang Lu, Christoph Weidenbach
article
31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland
Accès au bibtex
BibTex

2010

Conference papers

titre
The TLA+ Proof System: Building a Heterogeneous Verification Platform
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
International Conference on Theoretical Aspects of Computing – ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩
Accès au bibtex
BibTex

2008

Conference papers

titre
A TLA+ Proof System
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338299/file/main.pdf BibTex

Book sections

titre
The Specification Language TLA+
auteur
Stephan Merz
article
Dines Bjørner and Martin Henson. Logics of specification languages, Springer, pp.401-452, 2008, Monographs in Theoretical Computer Science, 978-3-540-74106-0
Accès au bibtex
BibTex