homepage
talks
research projects
student projects
events

Stephan Merz — publications

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Find my publications as seen by dblp or Google Scholar.


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, to appear (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, to appear (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, to appear (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]

Stephan Merz Last modified: Tue Mar 15 16:42:40 CET 2016