Stephan Merz — publications

Find my publications as seen by HAL, dblp or Google Scholar.

Extending PlusCal for Modeling Distributed Algorithms

Horatiu Cirstea and Stephan Merz
18th Intl. Conf. Integrated Formal Methods (iFM 2023).
© Springer (2023). [PDF]

Towards an Automatic Proof of the Bakery Algorithm

Aman Goel, Stephan Merz, and Karem Sakallah
43rd IFIP WG 6.1 Intl. Conf. Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2023).
© Springer (2023). [PDF]

Synchronization modulo P in Dynamic Networks

Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
Theoretical Computer Science, 2023. Extended version of our SSS 2021 paper.
© Elsevier (2023). [PDF]

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS

Igor Konnov, Markus Kuppe, and Stephan Merz
11th Intl. Symp. Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2022).
© Springer (2022). [PDF | TLA+ modules]

Correctness of a Set-Based Algorithm for Computing Strongly Connected Components of a Graph

Stephan Merz, Vincent Trélat
Archive of Formal Proofs, 2022. [Online version]

Prophecy Made Simple

Leslie Lamport and Stephan Merz
ACM Transactions on Programming Languages and Systems (TOPLAS) 44(2),6:1-6:27, 2022. [PDF]

Synchronization Modulo k in Dynamic Networks

Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
23rd Intl. Symp. Stabilization, Safety, and Security of Distributed Systems (SSS 2021). Best paper award.
© Springer (2021). [PDF]

Automated Orchestration of Security Chains Driven by Process Learning

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
Communication Networks and Service Management in the Era of Artificial Intelligence and Machine Learning.
© Wiley (2021). [PDF]

TLA+ Specifications and Proofs for Deconstructing the Bakery to Build a Distributed State Machine

Stephan Merz
Formal proof development, unpublished (2021).

An Extension of PlusCal for Modeling Distributed Algorithms

Heba Alkayed, Horatiu Cirstea, Stephan Merz
TLA+ Community Event 2020. [PDF | slides | presentation]

Formal specification and verification

Stephan Merz
In: Dahlia Malkhi (ed.), Concurrency: The Works of Leslie Lamport
© ACM (2019) [PDF]

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq, and Isabelle

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
10th Intl. Conf. Interactive Theorem Proving (ITP 2019)
[PDF]

Automated Factorization of Security Chains in Software-Defined Networks

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, and Stephan Merz
IFIP/IEEE Intl. Symp. Integrated Network Management (IM 2019)
© IEEE (2019) [PDF]

A Tool Suite for the Automated Synthesis of Security Function Chains

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, and Stephan Merz
IFIP/IEEE Intl. Symp. Integrated Network Management (IM 2019)
[PDF]

Integrating satisfiability solving in the assessment of system reliability modeled by dynamic fault trees

Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
29th Europ. Safety and Reliability Conf., ESREL 2019
[PDF]

Encoding TLA+ into unsorted and many-sorted first-order logic

Stephan Merz, Hernán Vanzetto
Science of Computer Programming 158, 2018.
© Elsevier (2018) [PDF]

A machine-checked correctness proof for Pastry

Noran Azmy, Stephan Merz, Christoph Weidenbach
Science of Computer Programming 158, 2018.
© Elsevier (2018) [PDF]

Generation of SDN policies for protecting android environments based on automata learning

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, and Stephan Merz
IEEE/IFIP Network Operations and Management Symp. (NOMS 2018)
© IEEE (2018) [PDF]

Synaptic: A formal checker for SDN-based security policies

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, and Stephan Merz
IEEE/IFIP Network Operations and Management Symp. (NOMS 2018)
© IEEE (2018) [PDF]

Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, and Stephan Merz
Elec. Comm. Europ. Assoc. Software Science and Technology 76 (Proc. AVoCS 2018).
[PDF]

Automated Verification of Security Chains in Software-Defined Networks with Synaptic

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, and Stephan Merz
IEEE Conf. on Network Softwarization (NetSoft 2017).
© IEEE (2017). [PDF]

Satisfiability Techniques for Computing Minimal Tie Sets in Reliability Assessment

Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, and Stephan Merz
10th Intl. Conf. Mathematical Techniques in Reliability (MMR 2017).
[PDF]

Proving Determinacy of the PharOS Real-Time Operating System

Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, and Stephan Merz
5th Intl. Conf. Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016).
© Springer, LNCS 9675, pp. 70-85 (2016). [PDF | TLA+ modules]

A Rigorous Correctness Proof for Pastry

Noran Azmy, Stephan Merz, and Christoph Weidenbach
5th Intl. Conf. Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016).
© Springer, LNCS 9675, pp. 86-101 (2016). [PDF | TLA+ modules]

Encoding TLA+ into Many-Sorted First-Order Logic

Stephan Merz and Hernán Vanzetto
5th Intl. Conf. Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016).
© Springer, LNCS 9675, pp. 54-69 (2016). [PDF]

Software component design with the B method – a formalization in Isabelle/HOL

David Déharbe and Stephan Merz
12th Intl. Conf. Formal Aspects of Component Software (FACS 2015)
© Springer, LNCS 9539, pp. 31-47 (2015). [PDF | Isabelle theories]

Modal Satisfiability via SMT Solving

Carlos Areces, Pascal Fontaine, and Stephan Merz
Software, Services, and Systems: Festschrift Martin Wirsing.
© Springer, LNCS 8950, pp. 30-45 (2015). [PDF]

Coalescing for Reasoning in First-Order Modal Logics

Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, and Stephan Merz
Intl. Wsh. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014). [PDF]

Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations

Jingshu Chen, Marie Duflot, and Stephan Merz
14th Intl. Wsh. Automated Verification of Critical Systems (AVoCS 2014).
© Elec. Comm. EASST vol. 70, 14 pages (2014). [PDF]

Refinement Types for TLA+

Stephan Merz and Hernán Vanzetto
6th Intl. Symp. NASA Formal Methods (NFM 2014).
© Springer, LNCS 8430, pp. 143-157 (2014). [PDF]

Towards Certifying Network Calculus

Etienne Mabille, Marc Boyer, Loïc Fejoz, and Stephan Merz
4th Intl. Conf. Interactive Theorem Proving (ITP 2013).
© Springer, LNCS 7998, pp. 484-489 (2013). [PDF]

Formal Verification of Distributed Algorithms

Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, and Josef Widder
Report on Dagstuhl Seminar 13141
Dagstuhl Reports 3(4):1-16, 2013. [PDF]

TLA+ Proofs

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
18th Intl. Symp. Formal Methods (FM 2012).
© Springer, LNCS 7436, pp. 147-154 (2012). [PDF | extended version | TLA+ module]

Combination of disjoint theories: beyond decidability

Pascal Fontaine, Stephan Merz, and Christoph Weidenbach
6th Intl. Joint Conf. on Automated Reasoning (IJCAR 2012).
© Springer, LNCS 7364, pp. 256-270 (2012). [PDF]

Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model

Henri Debrat and Stephan Merz
Archive of Formal Proofs, July 2012

Stuttering Equivalence Formalized in Isabelle/HOL

Stephan Merz
Archive of Formal Proofs, May 2012

Automatic Verification Of TLA+ Proof Obligations With SMT Solvers

Stephan Merz and Hernán Vanzetto
18th Intl. Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)
© Springer, LNCS 7180, pp. 289-303 (2012). [PDF]

Formal Verification of Consensus Algorithms Tolerating Malicious Faults

Bernadette Charron-Bost, Henri Debrat, and Stephan Merz
13th Intl. Symp. Stabilization, Safety, and Security of Distributed Systems (SSS 2011)
© Springer, LNCS 6976, pp. 120-134 (2011). [PDF]

Compression of Propositional Resolution Proofs via Partial Regularization

Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo
23rd Intl. Conf. Automated Deduction (CADE 2011).
© Springer, LNCS 6803, pp. 237-251 (2011). [PDF]

Exploiting Symmetry in SMT Problems

David Déharbe, Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo
23rd Intl. Conf. Automated Deduction (CADE 2011).
© Springer, LNCS 6803, pp. 222-236 (2011). [PDF]

Towards Verification of the Pastry Protocol Using TLA+

Tianxiang Lu, Stephan Merz, and Christoph Weidenbach
13th IFIP WG 6.1 Intl. Conf. Formal Techniques for Distributed Systems (FORTE 2011).
© Springer, LNCS 6722, pp. 244-258 (2011). [PDF]

SimGrid MC: Verification Support for a Multi-API Simulation Platform

Stephan Merz, Martin Quinson, and Cristian Rosa
13th IFIP WG 6.1 Intl. Conf. Formal Techniques for Distributed Systems (FORTE 2011).
© Springer, LNCS 6722, pp. 274-288 (2011). [PDF]

Verifying Safety Properties with the TLA+ Proof System

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz
5th Intl. Joint Conf. Automated Reasoning (IJCAR 2010).
© Springer, LNCS 6173, pp. 142-148 (2010). [PDF]

A High-Level Language for Modeling Algorithms and Their Properties

Sabina Akhtar, Stephan Merz, and Martin Quinson.
13th Brazilian Symposium on Formal Methods, SBMF 2010.
© Springer, LNCS 6527, pp. 49-63 (2010). [PDF]

A Simple Model of Communication APIs - Application to Dynamic Partial-order Reduction

Cristian Rosa, Stephan Merz, and Martin Quinson.
10th Intl. Workshop Automated Verification of Critical Systems (AVoCS 2010).
© Elec. Comm. Europ. Assoc. Software Science and Technology, ECEASST 35 [PDF]

Formal Verification of a Consensus Algorithm in the Heard-Of Model

Bernadette Charron-Bost and Stephan Merz
International Journal on Software and Informatics, vol.3 (2-3), pp. 273-304, 2009.
[PDF]
Typeset Isabelle proof script: PDF

Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL

Alexander Schimpf, Stephan Merz, and Jan-Georg Smaus
22nd Intl. Conf. Theorem Proving in Higher-Order Logics (TPHOLs 2009).
© Springer, LNCS 5674, pp. 424-439 (2009). [PDF]

A Formalization of the Semantics of Functional-Logic Programming in Isabelle

Francisco J. López-Fraguas, Stephan Merz, and Juan Rodríguez-Hortalá
22nd Intl. Conf. Theorem Proving in Higher-Order Logics (TPHOLs 2009). Emerging Trends Session.
[PDF]

A Reduction Theorem for the Verification of Round-Based Distributed Algorithms

Mouna Chaouch-Saad, Bernadette Charron-Bost, and Stephan Merz
LIX Colloquium Reachability Problems '09.
© Springer, LNCS 5797, pp. 93-106 (2009). [PDF]

Verified Incremental Development of Lock-Free Algorithms

David Déharbe, Loïc Fejoz, Pascal Fontaine and Stephan Merz
1st Luxembourg Day on Security and Reliability, February 2009.
Informal Workshop proceedings, [PDF]

A TLA+ Proof System

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz
LPAR 2008 Workshop Knowledge Exchange: Automated Provers and Proof Assistants.
CEUR Workshop Proceedings, vol. 418, pp. 17-37 (2008). [PDF]

The Specification Language TLA+

Stephan Merz
In: D. Bjørner, M. Henson (eds.): Logics of Specification Languages.
Springer Monographs in Theoretical Computer Science, pp. 401-451 (2008). [PDF]

An Introduction to Model Checking

Stephan Merz
In: S. Merz, N. Navet (eds.): Modeling and Verification of Real-Time Systems - Formalisms and Software Tools.
ISTE Publishing, pp. 77-109 (2008). [PDF]

Specification and Refinement of Access Control

Dominique Méry and Stephan Merz
Journal of Universal Computer Science 13(8), pp. 1073-1093 (2007). [PDF]
Extended version of Event Systems and Access Control.

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants

Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, and Alwen Tiu
12th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2006).
© Springer, LNCS 3920, pp. 167-181 (2006). [PDF]

Specification and Refinement of Mobile Systems in MTLA and Mobile UML

Alexander Knapp, Stephan Merz, Martin Wirsing, and Júlia Zappe
Theoretical Computer Science 351(2), pp. 184-202 (2006). [PDF]
Extended version of Refining Mobile UML State Machines.

Event Systems and Access Control

Dominique Méry and Stephan Merz
6th Intl. IFIP WG 1.7 Workshop on Issues in the Theory of Security (2006). [PDF]

Truly On-The-Fly LTL Model Checking

Moritz Hammer, Alexander Knapp, and Stephan Merz
11th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2005).
© Springer, LNCS 3440, pp. 191-205 (2005). [PDF]

Refining Mobile UML State Machines

Alexander Knapp, Stephan Merz, and Martin Wirsing.
10th Intl. Conf. Algebraic Methodology and Software Technology (AMAST 2004).
© Springer, LNCS (2004). [PDF]

TLA+ case study: a resource allocator

Stephan Merz
Technical report, LORIA, August 2004. [ZIP file containing PDF and TLA+ models]

Emptiness of Linear Weak Alternating Automata

Stephan Merz and Ali Sezgin.
Technical report, LORIA, December 2003. [PDF]

On the Logic of TLA+   (contains an error and is superseded by The Specification Language TLA+)

Stephan Merz.
Computers and Informatics, vol. 22, pp. 351-379 (2003).
(Special Issue on the semantics of specification formalisms, edited by Dines Bjørner.) [PDF]

A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems

Stephan Merz, Martin Wirsing, Júlia Zappe.
FASE 2003: Fundamental Approaches to Software Engineering. Warsaw, Poland.
© Springer, LNCS 2621, pp. 87-101 (2003). [PDF]

Model Checking Timed UML State Machines and Collaborations

Alexander Knapp, Stephan Merz, Christopher Rauh.
FTRTFT 2002: 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems. Oldenburg, Germany.
© Springer, LNCS 2469, pp. 395-414 (2002). [PDF]

Model Checking and Code Generation for UML State Machines and Collaborations

Alexander Knapp, Stephan Merz.
FM-TOOLS 2002: 5th Workshop on Tools for System Design and Verification.
Report 2002-11, Institut für Informatik, Universität Augsburg (2002). [PDF]

Logical Description and Analysis of Reactive Systems

Stephan Merz.
Habilitationsschrift, Universität München (2001). [ps.gz]

Model Checking UML State Machines and Collaborations

Timm Schäfer, Alexander Knapp, Stephan Merz.
CAV 2001 Workshop on Software Model Checking. Paris, France.
ENTCS 55(3) (2001). [PDF]

Model Checking: A Tutorial Overview

Stephan Merz.
F. Cassez et al. (eds): Modeling and Verification of Parallel Processes.
© Springer, LNCS 2067, pp. 3-38 (2001). [PDF]

Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams

Dominique Cansell, Dominique Méry, Stephan Merz.
Integrating Diagrammatic and Formal Specification Techniques (GI- / ÖCG-Jahrestagung). Vienna, Austria.
books@ocg.at 157/I, pp. 39-45 (2001). [PDF]

Diagram Refinements for the Design of Reactive Systems

Dominique Cansell, Dominique Méry, Stephan Merz.
© Springer, Journal of Universal Computer Science 7(2):159-174 (2001). [ps.gz]

Predicate Diagrams for the Verification of Reactive Systems

Dominique Cansell, Dominique Méry, Stephan Merz.
IFM 2000: 2nd Intl. Conference on Integrated Formal Methods. Berlin, Germany.
© Springer Verlag, LNCS 1945, pp. 380-397 (2000). [ps.gz]

Weak Alternating Automata in Isabelle/HOL

Stephan Merz.
TPHOLS 2000: 13th Intl. Conference on Theorem Proving and Higher Order Logics. Portland, Oregon.
© Springer, LNCS 1869, pp. 423-440 (2000). [ps.gz]

Verifying Reactive Systems Using Predicate Diagrams

Dominique Cansell, Dominique Méry, Stephan Merz.
FM-Tools 2000: 4th Workshop on Tools for System Design and Verification (extended abstract).
Ulmer Informatik-Berichte 2000-07, Universität Ulm (2000). [ps.gz]

A More Complete TLA

Stephan Merz.
FM'99: World Congress on Formal Methods. Toulouse, France.
© Springer, LNCS 1709, pp. 1226-1244 (1999). [ps.gz] (full version with proofs)

Animating TLA Specifications

Yassine Mokhtari, Stephan Merz.
LPAR'99: 6th Intl. Conf. on Logic for Programming and Automated Reasoning. Tbilisi, Georgia.
© Springer, LNCS 1705, pp. 92-110 (1999). [ps.gz]

Model Checking Techniques for the Analysis of Reactive Systems

Stephan Merz.
© Kluwer, Synthèse 133:173-201 (accepted 1999, appeared 2002) [ps.gz]

On the Verification of a Self-Stabilizing Algorithm

Stephan Merz.
Technical Report, University of Munich (1998). [ps.gz]

A User's Guide to TLA

Stephan Merz.
Modélisation et vérification des processus parallèles.
Ecole centrale de Nantes, pp. 29-44 (1998). [ps.gz]

Rules for Abstraction

Stephan Merz.
Advances in Computing Science - ASIAN'97. Kathmandu, Nepal.
© Springer, LNCS 1345, pp. 32-45 (1997). [ps.gz]

Type Checking Higher-Order Polymorphic Multi-Methods

François Bourdoncle, Stephan Merz.
POPL'97: 24th ACM Conference on Principles of Programming Languages. Paris, France.
ACM Press, pp. 302-315 (1997). [ps.gz]

Primitive subtyping /\ implicit polymorphism |= object-orientation

François Bourdoncle, Stephan Merz.
FOOL3: Workshop for Foundations of Object-Oriented Languages. New Brunswick, New Jersey (1996). [ps.gz]

On the integration of functional programming, class-based object-oriented programming, and multi-methods

François Bourdoncle, Stephan Merz.
Technical report, Ecole des Mines, Paris. [ps.gz]

On TLA as a logic

Martín Abadi, Stephan Merz.
© Springer, Deductive Program Design (M. Broy, ed). NATO ASI series F, pp. 235-272 (1996). [ps.gz]

The RPC-Memory Case Study: A Synopsis

Manfred Broy, Stephan Merz, Katharina Spies.
© Springer, LNCS 1169, pp. 5-20 (1996). [ps.gz]

A TLA solution to the RPC-Memory Specification Problem

Martín Abadi, Leslie Lamport, Stephan Merz.
© Springer, LNCS 1169, pp. 21-66 (1996). [ps.gz]

Steam boiler control specification problem: A TLA solution

Frank Leßke, Stephan Merz.
© Springer, LNCS 1165, pp. 339-359 (1996). [ps.gz]

An abstract account of composition

Martín Abadi, Stephan Merz.
MFCS'95: Mathematical Foundations of Computer Science. Praha, Czech Republic.
© Springer, LNCS 969, pp. 499-508 (1995). [ps.gz]

Mechanizing TLA in Isabelle

Stephan Merz.
Workshop Verification in New Orientations.
Technical Report, Univ. Maribor, Slovenia, 1995.
Superseded by the documentation for the Isabelle/TLA package.

Modular description and verification of concurrent objects

Jean-Paul Bahsoun, Stephan Merz, Corinne Servières.
0bject-Based Parallel and Distributed Computation. Tokyo, Japan.
© Springer, LNCS 1107, pp. 168-185 (1995). [ps.gz]

Une logique temporelle pour les objets concurrents, et sa procédure de décision

Jean-Paul Bahsoun, Stephan Merz, Corinne Servières.
Journées FAC'95 (Formalisation des Activités Concurrentes). Toulouse, France, 1995 [ps.gz]

Specifying and Verifying Fault-Tolerant Systems

Leslie Lamport, Stephan Merz.
FTRTFT'94: Formal Techniques in Real-Time and Fault-Tolerant Systems. Lübeck, Germany.
© Springer, LNCS 863, pp. 41-76 (1994). [ps.gz]

Efficiently executable temporal logic programs

Stephan Merz.
IJCAI Workshop Executable Modal and Temporal Logics.
© Springer, LNCS 897, pp. 69-85 (1994). [ps.gz]

From safety properties to temporal logic programming: A study in fixed point temporal logic

Stephan Merz.
Logica e filosofia delle scienze. Pisa: Edizioni ETS (1994). [ps.gz]

Temporal Logic as a Programming Language

Stephan Merz.
Ph.D. thesis and Technical report 9202, Ludwig-Maximilians-Universität München (1992). [ps.gz]

Decidability and Incompleteness Results for First-Order Temporal Logics of Linear Time

Stephan Merz.
Journal of Applied Non-Classical Logic 2(2), 1992 [ps.gz]