default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDStephan Merz
Person information
- affiliation: INRIA, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c63]Alessio Coltellacci, Stephan Merz, Gilles Dowek:
Reconstruction of SMT Proofs with Lambdapi. SMT@CAV 2024: 13-23- [i14]Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz:
Validating Traces of Distributed Programs Against TLA+ Specifications. CoRR abs/2404.16075 (2024) - 2023
- [j29]Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz:
Synchronization modulo P in dynamic networks. Theor. Comput. Sci. 942: 200-212 (2023) - [c62]Aman Goel, Stephan Merz, Karem A. Sakallah:
Towards an Automatic Proof of the Bakery Algorithm. FORTE 2023: 21-28 - [c61]Horatiu Cirstea, Stephan Merz:
Extending PlusCal for Modeling Distributed Algorithms. iFM 2023: 321-340 - 2022
- [j28]Stephan Merz, Vincent Trélat:
Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph. Arch. Formal Proofs 2022 (2022) - [j27]Leslie Lamport, Stephan Merz
:
Prophecy Made Simple. ACM Trans. Program. Lang. Syst. 44(2): 6:1-6:27 (2022) - [c60]Igor Konnov, Markus Kuppe, Stephan Merz:
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS. ISoLA (1) 2022: 88-105 - [i13]Igor Konnov, Markus Kuppe, Stephan Merz:
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS. CoRR abs/2211.07216 (2022) - 2021
- [c59]Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz:
Synchronization Modulo k in Dynamic Networks. SSS 2021: 425-439
2010 – 2019
- 2019
- [j26]Jasmin Christian Blanchette, Stephan Merz:
Selected Extended Papers of ITP 2016: Preface. J. Autom. Reason. 62(2): 169-170 (2019) - [c58]Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz:
Automated Factorization of Security Chains in Software-Defined Networks. IM 2019: 374-380 - [c57]Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz:
A Tool Suite for the Automated Synthesis of Security Function Chains. IM 2019: 716-717 - [c56]Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry:
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP 2019: 13:1-13:19 - [p1]Stephan Merz:
Formal specification and verification. Concurrency: the Works of Leslie Lamport 2019: 103-129 - 2018
- [j25]Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz:
Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 76 (2018) - [j24]Stephan Merz, Hernán Vanzetto:
Encoding TLA+ into unsorted and many-sorted first-order logic. Sci. Comput. Program. 158: 3-20 (2018) - [j23]Noran Azmy, Stephan Merz, Christoph Weidenbach:
A machine-checked correctness proof for Pastry. Sci. Comput. Program. 158: 64-80 (2018) - [c55]Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz:
Synaptic: A formal checker for SDN-based security policies. NOMS 2018: 1-2 - [c54]Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz:
Generation of SDN policies for protecting android environments based on automata learning. NOMS 2018: 1-7 - [i12]Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry:
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. CoRR abs/1810.11979 (2018) - 2017
- [c53]Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz:
Automated verification of security chains in software-defined networks with synaptic. NetSoft 2017: 1-9 - [i11]Leslie Lamport, Stephan Merz:
Auxiliary Variables in TLA+. CoRR abs/1703.05121 (2017) - 2016
- [j22]Stephan Merz, Jun Pang, Jin Song Dong:
Editorial. Formal Aspects Comput. 28(3): 343-344 (2016) - [j21]Stephan Merz, Jun Pang, Jin Song Dong:
Editorial. Formal Aspects Comput. 28(5): 723-724 (2016) - [c52]Stephan Merz, Hernán Vanzetto:
Encoding TLA ^+ + into Many-Sorted First-Order Logic. ABZ 2016: 54-69 - [c51]Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz:
Proving Determinacy of the PharOS Real-Time Operating System. ABZ 2016: 70-85 - [c50]Noran Azmy, Stephan Merz, Christoph Weidenbach:
A Rigorous Correctness Proof for Pastry. ABZ 2016: 86-101 - [e6]Jasmin Christian Blanchette, Stephan Merz:
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Lecture Notes in Computer Science 9807, Springer 2016, ISBN 978-3-319-43143-7 [contents] - 2015
- [c49]Carlos Areces, Pascal Fontaine, Stephan Merz:
Modal Satisfiability via SMT Solving. Software, Services, and Systems 2015: 30-45 - [c48]David Déharbe, Stephan Merz:
Software Component Design with the B Method - A Formalization in Isabelle/HOL. FACS 2015: 31-47 - [i10]Stephan Merz, Hernán Vanzetto:
Encoding TLA+ set theory into many-sorted first-order logic. CoRR abs/1508.03838 (2015) - 2014
- [j20]Jingshu Chen, Marie Duflot, Stephan Merz:
Analyzing Conflict Freedom for Multi-threaded Programs With Time Annotations. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014) - [j19]Gerald Lüttgen, Stephan Merz:
Special issue on Automated Verification of Critical Systems (AVoCS'12). Sci. Comput. Program. 96: 277-278 (2014) - [c47]Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz:
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. ARQNL@IJCAR 2014: 1-16 - [c46]Stephan Merz, Hernán Vanzetto:
Refinement Types for tla +. NASA Formal Methods 2014: 143-157 - [e5]Stephan Merz, Jun Pang:
Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings. Lecture Notes in Computer Science 8829, Springer 2014, ISBN 978-3-319-11736-2 [contents] - [i9]Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz:
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. CoRR abs/1409.3819 (2014) - [i8]Jingshu Chen, Marie Duflot, Stephan Merz:
Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations. CoRR abs/1412.0961 (2014) - 2013
- [c45]Etienne Mabille, Marc Boyer, Loïc Fejoz, Stephan Merz:
Towards Certifying Network Calculus. ITP 2013: 484-489 - [i7]Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder:
Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). Dagstuhl Reports 3(4): 1-16 (2013) - 2012
- [j18]Henri Debrat, Stephan Merz:
Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model. Arch. Formal Proofs 2012 (2012) - [j17]Stephan Merz:
Stuttering Equivalence. Arch. Formal Proofs 2012 (2012) - [j16]Gerald Lüttgen, Stephan Merz:
Preface. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012) - [j15]Stephan Merz, Hernán Vanzetto:
Harnessing SMT Solvers for TLA+ Proofs. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012) - [c44]Pascal Fontaine, Stephan Merz, Christoph Weidenbach:
Combination of Disjoint Theories: Beyond Decidability. IJCAR 2012: 256-270 - [c43]Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto:
TLA + Proofs. FM 2012: 147-154 - [c42]Stephan Merz, Hernán Vanzetto:
Automatic Verification of TLA + Proof Obligations with SMT Solvers. LPAR 2012: 289-303 - [c41]Stephan Merz:
Proofs and Proof Certification in the TLA+ Proof System. PxTP 2012: 16-20 - [i6]Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto:
TLA+ Proofs. CoRR abs/1208.5933 (2012) - 2011
- [j14]Gudmund Grov, Stephan Merz:
A Definitional Encoding of TLA* in Isabelle/HOL. Arch. Formal Proofs 2011 (2011) - [c40]David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo:
Exploiting Symmetry in SMT Problems. CADE 2011: 222-236 - [c39]Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo:
Compression of Propositional Resolution Proofs via Partial Regularization. CADE 2011: 237-251 - [c38]Tianxiang Lu, Stephan Merz, Christoph Weidenbach:
Towards Verification of the Pastry Protocol Using TLA + . FMOODS/FORTE 2011: 244-258 - [c37]Stephan Merz, Martin Quinson, Cristian Daniel Rosa:
SimGrid MC: Verification Support for a Multi-API Simulation Platform. FMOODS/FORTE 2011: 274-288 - [c36]Stephan Merz, Hernán Vanzetto:
Towards certification of TLA+ proof obligations with SMT solvers. PxTP 2011: 40-45 - [c35]Bernadette Charron-Bost, Henri Debrat, Stephan Merz:
Formal Verification of Consensus Algorithms Tolerating Malicious Faults. SSS 2011: 120-134 - 2010
- [j13]Hehua Zhang, Stephan Merz, Ming Gu:
Specifying and verifying PLC systems with TLA+ : A case study. Comput. Math. Appl. 60(3): 695-705 (2010) - [j12]Cristian Daniel Rosa, Stephan Merz, Martin Quinson:
A Simple Model of Communication APIs - Application to Dynamic Partial-order Reduction. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 35 (2010) - [c34]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
Verifying Safety Properties with the TLA+ Proof System. IJCAR 2010: 142-148 - [c33]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
The TLA+ Proof System: Building a Heterogeneous Verification Platform. ICTAC 2010: 44 - [c32]Sabina Akhtar, Stephan Merz, Martin Quinson:
A High-Level Language for Modeling Algorithms and Their Properties. SBMF 2010: 49-63 - [e4]Dominique Méry, Stephan Merz:
Integrated Formal Methods - 8th International Conference, IFM 2010, Nancy, France, October 11-14, 2010. Proceedings. Lecture Notes in Computer Science 6396, Springer 2010, ISBN 978-3-642-16264-0 [contents] - [i5]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
Verifying Safety Properties With the TLA+ Proof System. CoRR abs/1011.2560 (2010)
2000 – 2009
- 2009
- [j11]Bernadette Charron-Bost, Stephan Merz:
Formal Verification of a Consensus Algorithm in the Heard-Of Model. Int. J. Softw. Informatics 3(2-3): 273-303 (2009) - [c31]Mouna Chaouch-Saad, Bernadette Charron-Bost, Stephan Merz:
A Reduction Theorem for the Verification of Round-Based Distributed Algorithms. RP 2009: 93-106 - [c30]Hehua Zhang, Stephan Merz, Ming Gu:
Specifying and Verifying PLC Systems with TLA+. TASE 2009: 293-294 - [c29]Alexander Schimpf, Stephan Merz, Jan-Georg Smaus:
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. TPHOLs 2009: 424-439 - [i4]Francisco Javier López-Fraguas, Stephan Merz, Juan Rodríguez-Hortalá:
A Formalization of the Semantics of Functional-Logic Programming in Isabelle. CoRR abs/0908.0494 (2009) - 2008
- [b2]Fred Kröger, Stephan Merz:
Temporal Logic and State Systems. Texts in Theoretical Computer Science. An EATCS Series, Springer 2008, ISBN 978-3-540-67401-6, pp. 1-433 - [j10]Serge Autexier, Heiko Mantel, Stephan Merz, Tobias Nipkow:
Preface. J. Autom. Reason. 41(3-4): 191-192 (2008) - [c28]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
A TLA+ Proof System. LPAR Workshops 2008 - [i3]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
A TLA+ Proof System. CoRR abs/0811.1914 (2008) - 2007
- [j9]Eun-Young Kang, Stephan Merz:
Predicate diagrams for the verification of real-time systems. Formal Aspects Comput. 19(3): 401-413 (2007) - [j8]Dominique Méry, Stephan Merz:
Specification and Refinement of Access Control. J. Univers. Comput. Sci. 13(8): 1073-1093 (2007) - [e3]Stephan Merz, Tobias Nipkow:
Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, AVoCS 2006, Nancy, France, September 18-19, 2006. Electronic Notes in Theoretical Computer Science 185, Elsevier 2007 [contents] - 2006
- [j7]Alexander Knapp, Stephan Merz, Martin Wirsing, Júlia Zappe:
Specification and refinement of mobile systems in MTLA and mobile UML. Theor. Comput. Sci. 351(2): 184-202 (2006) - [c27]Serge Autexier, Stephan Merz, Leendert W. N. van der Torre, Reinhard Wilhelm, Pierre Wolper:
Preface -- Workshop Trustworthy Software 2006. Trustworthy Software 2006 - [c26]Houda Fekih, Leila Jemni Ben Ayed, Stephan Merz:
Transformation of B specifications into UML class diagrams and state machines. SAC 2006: 1840-1844 - [c25]Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu:
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. TACAS 2006: 167-181 - [c24]Stephan Merz, Tobias Nipkow:
Preface. AVoCS 2006: 1-2 - [e2]Serge Autexier, Stephan Merz, Leendert W. N. van der Torre, Reinhard Wilhelm, Pierre Wolper:
Workshop "Trustworthy Software" 2006, May 18-19, 2006, Saarland University, Saarbrücken, Germany. OASIcs 3, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2006 [contents] - [i2]Dominique Méry, Stephan Merz:
Event Systems and Access Control. CoRR abs/cs/0604081 (2006) - 2005
- [j6]Mauro Jaskelioff, Stephan Merz:
Proving the Correctness of Disk Paxos. Arch. Formal Proofs 2005 (2005) - [c23]Moritz Hammer, Alexander Knapp, Stephan Merz:
Truly On-the-Fly LTL Model Checking. TACAS 2005: 191-205 - [c22]Eun-Young Kang, Stephan Merz:
Predicate Diagrams for the Verification of Real-Time Systems. AVoCS 2005: 151-165 - [i1]Moritz Hammer, Alexander Knapp, Stephan Merz:
Truly On-The-Fly LTL Model Checking. CoRR abs/cs/0511061 (2005) - 2004
- [c21]Alexander Knapp, Stephan Merz, Martin Wirsing:
Refining Mobile UML State Machines. AMAST 2004: 274-288 - 2003
- [j5]Stephan Merz:
On the Logic of TLA+. Comput. Artif. Intell. 22(3-4): 351-379 (2003) - [c20]Stephan Merz, Martin Wirsing, Júlia Zappe:
A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems. FASE 2003: 87-101 - 2002
- [j4]Stephan Merz:
Model Checking Techniqes for the Analysis of Reactive Systems. Synth. 133(1-2): 173-201 (2002) - [c19]Alexander Knapp, Stephan Merz, Christopher Rauh:
Model Checking - Timed UML State Machines and Collaborations. FTRTFT 2002: 395-416 - 2001
- [j3]Dominique Cansell, Dominique Méry, Stephan Merz:
Diagram Refinements for the Design of Reactive Systems. J. Univers. Comput. Sci. 7(2): 159-174 (2001) - [c18]Dominique Cansell, Dominique Méry, Stephan Merz:
Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams. GI Jahrestagung (1) 2001: 628-634 - [c17]Timm Schäfer, Alexander Knapp, Stephan Merz:
Model checking UML state machines and collaborations. Workshop on Software Model Checking @ CAV 2001: 357-369 - 2000
- [c16]Dominique Cansell, Dominique Méry, Stephan Merz:
Predicate Diagrams for the Verification of Reactive Systems. IFM 2000: 380-397 - [c15]Stephan Merz:
Model Checking: A Tutorial Overview. MOVEP 2000: 3-38 - [c14]Stephan Merz:
Weak Alternating Automata in Isabelle/HOL. TPHOLs 2000: 424-441
1990 – 1999
- 1999
- [c13]Stephan Merz:
A More Complete TLA. World Congress on Formal Methods 1999: 1226-1244 - [c12]Yassin Mokhtari, Stephan Merz:
Animating TLA Specifications. LPAR 1999: 92-110 - 1997
- [c11]Stephan Merz:
Rules for Abstraction. ASIAN 1997: 32-45 - [c10]François Bourdoncle, Stephan Merz:
Type-Checking Higher-Order Polymorphic Multi-Methods. POPL 1997: 302-315 - 1996
- [c9]Martín Abadi, Stephan Merz:
On TLA as a logic. NATO ASI DPD 1996: 235-271 - [e1]Manfred Broy, Stephan Merz, Katharina Spies:
Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994). Lecture Notes in Computer Science 1169, Springer 1996, ISBN 3-540-61984-4 [contents] - 1995
- [c8]Frank Leßke, Stephan Merz:
Steam Boiler Control Specification Problem: A TLA Solution. Formal Methods for Industrial Applications 1995: 339-358 - [c7]Martín Abadi, Stephan Merz:
An Abstract Account of Composition. MFCS 1995: 499-508 - [c6]Jean Paul Bahsoun, Stephan Merz, Corinne Servieres:
Modular Description and Verification of Concurrent Objects. OBPDC 1995: 168-186 - 1994
- [c5]Manfred Broy, Stephan Merz, Katharina Spies:
The RPC-Memory Case Study: A Synopsis. Formal Systems Specification 1994: 5-20 - [c4]Martín Abadi, Leslie Lamport, Stephan Merz:
A TLA Solution to the RPC-Memory Specification Problem. Formal Systems Specification 1994: 21-66 - [c3]Leslie Lamport, Stephan Merz:
Specifying and Verifying Fault-Tolerant Systems. FTRTFT 1994: 41-76 - 1993
- [c2]Stephan Merz:
Efficiently Executable Temporal Logic Programs. Executable Modal and Temporal Logics 1993: 69-85 - [c1]Jean Paul Bahsoun, Stephan Merz, Corinne Servieres:
A Framework for Programming and Formalizing Concurrent Objects. SIGSOFT FSE 1993: 126-137 - 1992
- [b1]Stephan Merz:
Temporal logic as a programming language. Ludwig Maximilian University of Munich, Germany, 1992, pp. 1-202 - [j2]Stephan Merz:
Decidability and incompleteness results for first-order temporal logics of linear time. J. Appl. Non Class. Logics 2(2): 139-156 (1992) - 1991
- [j1]Fred Kröger, Stephan Merz:
Temporal logic and recursion. Fundam. Informaticae 14(2): 261-281 (1991)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:25 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
