We stand with Ukraine

We stand with Ukraine

Stephan Merz

Orcid: 0000-0003-0974-1844

Affiliations:

INRIA, France

According to our database¹, Stephan Merz authored at least 99 papers between 1991 and 2023.

Collaborative distances:

Dijkstra number² of two.
Erdős number³ of three.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Links

Online presence:

On csauthors.net:

Bibliography

2023

Synchronization modulo <i>P</i> in dynamic networks.

[BibT_eX]

[DOI]

Louis Penet de Monterno

,

Bernadette Charron-Bost

,

Theor. Comput. Sci., 2023

Extending PlusCal for Modeling Distributed Algorithms.

[BibT_eX]

[DOI]

Horatiu Cirstea

,

Proceedings of the iFM 2023 - 18th International Conference, 2023

Towards an Automatic Proof of the Bakery Algorithm.

[BibT_eX]

[DOI]

,

,

Karem A. Sakallah

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2023

2022

Prophecy Made Simple.

[BibT_eX]

[DOI]

,

ACM Trans. Program. Lang. Syst., 2022

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

[BibT_eX]

[DOI]

,

,

CoRR, 2022

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

[BibT_eX]

[DOI]

,

Vincent Trélat

Arch. Formal Proofs, 2022

Specification and Verification with the TLA<sup>+</sup> Trifecta: TLC, Apalache, and TLAPS.

[BibT_eX]

[DOI]

,

,

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

2021

Synchronization Modulo k in Dynamic Networks.

[BibT_eX]

[DOI]

Louis Penet de Monterno

,

Bernadette Charron-Bost

,

Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2021

2019

Selected Extended Papers of ITP 2016: Preface.

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

,

J. Autom. Reason., 2019

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

[BibT_eX]

[DOI]

,

,

Jean-Jacques Lévy

,

,

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

A Tool Suite for the Automated Synthesis of Security Function Chains.

[BibT_eX]

[DOI]

Nicolas Schnepf

,

,

Abdelkader Lahmadi

,

Proceedings of the IFIP/IEEE International Symposium on Integrated Network Management, 2019

Automated Factorization of Security Chains in Software-Defined Networks.

[BibT_eX]

[DOI]

Nicolas Schnepf

,

,

Abdelkader Lahmadi

,

Proceedings of the IFIP/IEEE International Symposium on Integrated Network Management, 2019

Formal specification and verification.

[BibT_eX]

[DOI]

Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

2018

Encoding TLA<sup>+</sup> into unsorted and many-sorted first-order logic.

[BibT_eX]

[DOI]

,

Hernán Vanzetto

Sci. Comput. Program., 2018

A machine-checked correctness proof for Pastry.

[BibT_eX]

[DOI]

,

,

Christoph Weidenbach

Sci. Comput. Program., 2018

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

[BibT_eX]

[DOI]

Nicolas Schnepf

,

,

Abdelkader Lahmadi

,

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle.

[BibT_eX]

[DOI]

,

,

Jean-Jacques Lévy

,

,

CoRR, 2018

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

[BibT_eX]

[DOI]

Nicolas Schnepf

,

,

Abdelkader Lahmadi

,

Proceedings of the 2018 IEEE/IFIP Network Operations and Management Symposium, 2018

Synaptic: A formal checker for SDN-based security policies.

[BibT_eX]

[DOI]

Nicolas Schnepf

,

,

Abdelkader Lahmadi

,

Proceedings of the 2018 IEEE/IFIP Network Operations and Management Symposium, 2018

2017

Auxiliary Variables in TLA+.

[BibT_eX]

[DOI]

,

CoRR, 2017

Automated verification of security chains in software-defined networks with synaptic.

[BibT_eX]

[DOI]

Nicolas Schnepf

,

,

Abdelkader Lahmadi

,

Proceedings of the 2017 IEEE Conference on Network Softwarization, 2017

2016

Editorial.

[BibT_eX]

[DOI]

,

,

Formal Aspects Comput., 2016

Encoding TLA ^+ + into Many-Sorted First-Order Logic.

[BibT_eX]

[DOI]

,

Hernán Vanzetto

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

A Rigorous Correctness Proof for Pastry.

[BibT_eX]

[DOI]

,

,

Christoph Weidenbach

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Proving Determinacy of the PharOS Real-Time Operating System.

[BibT_eX]

[DOI]

,

,

Matthieu Lemerre

,

,

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

2015

Encoding TLA+ set theory into many-sorted first-order logic.

[BibT_eX]

[DOI]

,

Hernán Vanzetto

CoRR, 2015

Software Component Design with the B Method - A Formalization in Isabelle/HOL.

[BibT_eX]

[DOI]

,

Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

Modal Satisfiability via SMT Solving.

[BibT_eX]

[DOI]

,

Pascal Fontaine

,

Proceedings of the Software, 2015

2014

Special issue on Automated Verification of Critical Systems (AVoCS'12).

[BibT_eX]

[DOI]

Gerald Lüttgen

,

Sci. Comput. Program., 2014

Analyzing Conflict Freedom for Multi-threaded Programs With Time Annotations.

[BibT_eX]

[DOI]

,

,

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014

Refinement Types for tla +.

[BibT_eX]

[DOI]

,

Hernán Vanzetto

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics.

[BibT_eX]

[DOI]

,

,

,

,

Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 2014

2013

Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141).

[BibT_eX]

[DOI]

Bernadette Charron-Bost

,

,

Andrey Rybalchenko

,

Dagstuhl Reports, 2013

Towards Certifying Network Calculus.

[BibT_eX]

[DOI]

Etienne Mabille

,

,

,

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Harnessing SMT Solvers for TLA+ Proofs.

[BibT_eX]

[DOI]

,

Hernán Vanzetto

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Preface.

[BibT_eX]

[DOI]

Gerald Lüttgen

,

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Stuttering Equivalence.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2012

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

[BibT_eX]

[DOI]

,

Arch. Formal Proofs, 2012

Proofs and Proof Certification in the TLA<sup>+</sup> Proof System.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

Automatic Verification of TLA + Proof Obligations with SMT Solvers.

[BibT_eX]

[DOI]

,

Hernán Vanzetto

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

TLA + Proofs.

[BibT_eX]

[DOI]

Denis Cousineau

,

,

,

,

Daniel Ricketts

,

Hernán Vanzetto

Proceedings of the FM 2012: Formal Methods, 2012

Combination of Disjoint Theories: Beyond Decidability.

[BibT_eX]

[DOI]

Pascal Fontaine

,

,

Christoph Weidenbach

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

A Definitional Encoding of TLA* in Isabelle/HOL.

[BibT_eX]

[DOI]

,

Arch. Formal Proofs, 2011

Formal Verification of Consensus Algorithms Tolerating Malicious Faults.

[BibT_eX]

[DOI]

Bernadette Charron-Bost

,

,

Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2011

Towards certification of TLA+ proof obligations with SMT solvers.

[BibT_eX]

[DOI]

,

Hernán Vanzetto

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

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

[BibT_eX]

[DOI]

,

,

Cristian Daniel Rosa

Proceedings of the Formal Techniques for Distributed Systems, 2011

Towards Verification of the Pastry Protocol Using TLA<sup> + </sup>.

[BibT_eX]

[DOI]

,

,

Christoph Weidenbach

Proceedings of the Formal Techniques for Distributed Systems, 2011

Compression of Propositional Resolution Proofs via Partial Regularization.

[BibT_eX]

[DOI]

Pascal Fontaine

,

,

Bruno Woltzenlogel Paleo

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Exploiting Symmetry in SMT Problems.

[BibT_eX]

[DOI]

,

Pascal Fontaine

,

,

Bruno Woltzenlogel Paleo

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

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

[BibT_eX]

[DOI]

Cristian Daniel Rosa

,

,

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Specifying and verifying PLC systems with TLA<sup>+</sup> : A case study.

[BibT_eX]

[DOI]

,

,

Comput. Math. Appl., 2010

A High-Level Language for Modeling Algorithms and Their Properties.

[BibT_eX]

[DOI]

,

,

Proceedings of the Formal Methods: Foundations and Applications, 2010

The TLA<sup>+</sup> Proof System: Building a Heterogeneous Verification Platform.

[BibT_eX]

[DOI]

Kaustuv Chaudhuri

,

,

,

Proceedings of the Theoretical Aspects of Computing, 2010

Verifying Safety Properties with the TLA+ Proof System.

[BibT_eX]

[DOI]

Kaustuv Chaudhuri

,

,

,

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

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

[BibT_eX]

[DOI]

Bernadette Charron-Bost

,

Int. J. Softw. Informatics, 2009

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

[BibT_eX]

[DOI]

Francisco Javier López-Fraguas

,

,

Juan Rodríguez-Hortalá

CoRR, 2009

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

[BibT_eX]

[DOI]

Alexander Schimpf

,

,

Jan-Georg Smaus

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Specifying and Verifying PLC Systems with TLA+.

[BibT_eX]

[DOI]

,

,

Proceedings of the TASE 2009, 2009

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

[BibT_eX]

[DOI]

Mouna Chaouch-Saad

,

Bernadette Charron-Bost

,

Proceedings of the Reachability Problems, 3rd International Workshop, 2009

2008

Temporal Logic and State Systems

[BibT_eX]

[DOI]

,

Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-68635-4, 2008

Preface.

[BibT_eX]

[DOI]

,

,

,

J. Autom. Reason., 2008

A TLA+ Proof System.

[BibT_eX]

[DOI]

Kaustuv Chaudhuri

,

,

,

Proceedings of the LPAR 2008 Workshops, 2008

2007

Specification and Refinement of Access Control.

[BibT_eX]

[DOI]

Dominique Méry

,

J. Univers. Comput. Sci., 2007

2006

Specification and refinement of mobile systems in MTLA and mobile UML.

[BibT_eX]

[DOI]

Alexander Knapp

,

,

,

Theor. Comput. Sci., 2006

Preface.

[BibT_eX]

[DOI]

,

Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, 2006

Event Systems and Access Control

[BibT_eX]

[DOI]

Dominique Méry

,

CoRR, 2006

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

[BibT_eX]

[DOI]

Pascal Fontaine

,

Jean-Yves Marion

,

,

Leonor Prensa Nieto

,

Alwen Fernanto Tiu

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Transformation of B specifications into UML class diagrams and state machines.

[BibT_eX]

[DOI]

,

Leila Jemni Ben Ayed

,

Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), 2006

Preface -- Workshop Trustworthy Software 2006.

[BibT_eX]

[DOI]

,

,

Leendert W. N. van der Torre

,

Reinhard Wilhelm

,

Proceedings of the Workshop "Trustworthy Software" 2006, 2006

2005

Predicate Diagrams for the Verification of Real-Time Systems.

[BibT_eX]

[DOI]

,

Proceedings of the 5th International Workshop on Automated Verification of Critical Systems, 2005

Proving the Correctness of Disk Paxos.

[BibT_eX]

[DOI]

Mauro Jaskelioff

,

Arch. Formal Proofs, 2005

Truly On-the-Fly LTL Model Checking.

[BibT_eX]

[DOI]

,

Alexander Knapp

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

2004

Refining Mobile UML State Machines.

[BibT_eX]

[DOI]

Alexander Knapp

,

,

Proceedings of the Algebraic Methodology and Software Technology, 2004

2003

On the Logic of TLA+.

[BibT_eX]

[DOI]

Comput. Artif. Intell., 2003

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

[BibT_eX]

[DOI]

,

,

Proceedings of the Fundamental Approaches to Software Engineering, 2003

2002

Model Checking Techniqes for the Analysis of Reactive Systems.

[BibT_eX]

[DOI]

Synth., 2002

Model Checking - Timed UML State Machines and Collaborations.

[BibT_eX]

[DOI]

Alexander Knapp

,

,

Christopher Rauh

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

2001

Diagram Refinements for the Design of Reactive Systems.

[BibT_eX]

[DOI]

Dominique Cansell

,

Dominique Méry

,

J. Univers. Comput. Sci., 2001

Model checking UML state machines and collaborations.

[BibT_eX]

[DOI]

,

Alexander Knapp

,

Proceedings of the Workshop on Software Model Checking 2001, 2001

Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams.

[BibT_eX]

Dominique Cansell

,

Dominique Méry

,

Proceedings of the Tagungsband der GI/OCG-Jahrestagung - 31. Jahrestagung der Gesellschaft für Informatik, Wirtschaft und Wissenschaft in der Network Economy, 2001

2000

Weak Alternating Automata in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Model Checking: A Tutorial Overview.

[BibT_eX]

[DOI]

Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

Predicate Diagrams for the Verification of Reactive Systems.

[BibT_eX]

[DOI]

Dominique Cansell

,

Dominique Méry

,

Proceedings of the Integrated Formal Methods, Second International Conference, 2000

1999

Animating TLA Specifications.

[BibT_eX]

[DOI]

Yassin Mokhtari

,

Proceedings of the Logic Programming and Automated Reasoning, 6th International Conference, 1999

A More Complete TLA.

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

1997

Type-Checking Higher-Order Polymorphic Multi-Methods.

[BibT_eX]

[DOI]

François Bourdoncle

,

Proceedings of the Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

Rules for Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computing Science, 1997

1996

On TLA as a logic.

[BibT_eX]

,

Proceedings of the NATO Advanced Study Institute on Deductive Program Design, 1996

1995

Modular Description and Verification of Concurrent Objects.

[BibT_eX]

[DOI]

Jean Paul Bahsoun

,

,

Corinne Servieres

Proceedings of the Object-Based Parallel and Distributed Computation, 1995

An Abstract Account of Composition.

[BibT_eX]

[DOI]

,

Proceedings of the Mathematical Foundations of Computer Science 1995, 1995

Steam Boiler Control Specification Problem: A TLA Solution.

[BibT_eX]

[DOI]

,

Proceedings of the Formal Methods for Industrial Applications, 1995

1994

Specifying and Verifying Fault-Tolerant Systems.

[BibT_eX]

[DOI]

,

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

The RPC-Memory Case Study: A Synopsis.

[BibT_eX]

[DOI]

,

,

Katharina Spies

Proceedings of the Formal Systems Specification, 1994

A TLA Solution to the RPC-Memory Specification Problem.

[BibT_eX]

[DOI]

,

,

Proceedings of the Formal Systems Specification, 1994

1993

A Framework for Programming and Formalizing Concurrent Objects.

[BibT_eX]

[DOI]

Jean Paul Bahsoun

,

,

Corinne Servieres

Proceedings of the First ACM SIGSOFT Symposium on Foundations of Software Engineering, 1993

Efficiently Executable Temporal Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Executable Modal and Temporal Logics, 1993

1992

Temporal logic as a programming language.

[BibT_eX]

[DOI]

PhD thesis, 1992

Decidability and incompleteness results for first-order temporal logics of linear time.

[BibT_eX]

[DOI]

J. Appl. Non Class. Logics, 1992

1991

Temporal logic and recursion.

[BibT_eX]

,

Fundam. Informaticae, 1991

Loading...