Stephan Merz

According to our database1, Stephan Merz authored at least 80 papers between 1991 and 2018.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2018
Encoding TLA+ into unsorted and many-sorted first-order logic.
Sci. Comput. Program., 2018

A machine-checked correctness proof for Pastry.
Sci. Comput. Program., 2018

Generation of SDN policies for protecting android environments based on automata learning.
Proceedings of the 2018 IEEE/IFIP Network Operations and Management Symposium, 2018

Synaptic: A formal checker for SDN-based security policies.
Proceedings of the 2018 IEEE/IFIP Network Operations and Management Symposium, 2018

2017
Automated verification of security chains in software-defined networks with synaptic.
Proceedings of the 2017 IEEE Conference on Network Softwarization, 2017

2016
Editorial.
Formal Asp. Comput., 2016

Editorial.
Formal Asp. Comput., 2016

Encoding TLA ^+ + into Many-Sorted First-Order Logic.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

A Rigorous Correctness Proof for Pastry.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Proving Determinacy of the PharOS Real-Time Operating System.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

2015
Software Component Design with the B Method - A Formalization in Isabelle/HOL.
Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

Modal Satisfiability via SMT Solving.
Proceedings of the Software, 2015

2014
Special issue on Automated Verification of Critical Systems (AVoCS'12).
Sci. Comput. Program., 2014

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

Refinement Types for tla +.
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.
Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 2014

2013
Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141).
Dagstuhl Reports, 2013

Towards Certifying Network Calculus.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012
Harnessing SMT Solvers for TLA+ Proofs.
ECEASST, 2012

Preface.
ECEASST, 2012

Stuttering Equivalence.
Archive of Formal Proofs, 2012

Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model.
Archive of Formal Proofs, 2012

Automatic Verification of TLA + Proof Obligations with SMT Solvers.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

TLA + Proofs.
Proceedings of the FM 2012: Formal Methods, 2012

Combination of Disjoint Theories: Beyond Decidability.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011
A Definitional Encoding of TLA* in Isabelle/HOL.
Archive of Formal Proofs, 2011

Formal Verification of Consensus Algorithms Tolerating Malicious Faults.
Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2011

SimGrid MC: Verification Support for a Multi-API Simulation Platform.
Proceedings of the Formal Techniques for Distributed Systems, 2011

Towards Verification of the Pastry Protocol Using TLA + .
Proceedings of the Formal Techniques for Distributed Systems, 2011

Compression of Propositional Resolution Proofs via Partial Regularization.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Exploiting Symmetry in SMT Problems.
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.
ECEASST, 2010

Specifying and verifying PLC systems with TLA+ : A case study.
Computers & Mathematics with Applications, 2010

A High-Level Language for Modeling Algorithms and Their Properties.
Proceedings of the Formal Methods: Foundations and Applications, 2010

The TLA+ Proof System: Building a Heterogeneous Verification Platform.
Proceedings of the Theoretical Aspects of Computing, 2010

Verifying Safety Properties with the TLA+ Proof System.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Formal Verification of a Consensus Algorithm in the Heard-Of Model.
Int. J. Software and Informatics, 2009

Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Specifying and Verifying PLC Systems with TLA+.
Proceedings of the TASE 2009, 2009

A Reduction Theorem for the Verification of Round-Based Distributed Algorithms.
Proceedings of the Reachability Problems, 3rd International Workshop, 2009

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

Preface.
J. Autom. Reasoning, 2008

A TLA+ Proof System.
Proceedings of the LPAR 2008 Workshops, 2008

2007
Specification and Refinement of Access Control.
J. UCS, 2007

Predicate diagrams for the verification of real-time systems.
Formal Asp. Comput., 2007

Preface.
Electr. Notes Theor. Comput. Sci., 2007

2006
Specification and refinement of mobile systems in MTLA and mobile UML.
Theor. Comput. Sci., 2006

Predicate Diagrams for the Verification of Real-Time Systems.
Electr. Notes Theor. Comput. Sci., 2006

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.
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.
Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), 2006

Preface -- Workshop Trustworthy Software 2006.
Proceedings of the Workshop "Trustworthy Software" 2006, 2006

2005
Proving the Correctness of Disk Paxos.
Archive of Formal Proofs, 2005

Truly On-the-Fly LTL Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

2004
Refining Mobile UML State Machines.
Proceedings of the Algebraic Methodology and Software Technology, 2004

2003
On the Logic of TLA+.
Computers and Artificial Intelligence, 2003

A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems.
Proceedings of the Fundamental Approaches to Software Engineering, 2003

2002
Model Checking Techniqes for the Analysis of Reactive Systems.
Synthese, 2002

Model Checking - Timed UML State Machines and Collaborations.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

2001
Diagram Refinements for the Design of Reactive Systems.
J. UCS, 2001

Model checking UML state machines and collaborations.
Electr. Notes Theor. Comput. Sci., 2001

Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams.
GI Jahrestagung (1), 2001

2000
Weak Alternating Automata in Isabelle/HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Model Checking: A Tutorial Overview.
Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

Predicate Diagrams for the Verification of Reactive Systems.
Proceedings of the Integrated Formal Methods, Second International Conference, 2000

1999
Animating TLA Specifications.
Proceedings of the Logic Programming and Automated Reasoning, 6th International Conference, 1999

A More Complete TLA.
Proceedings of the FM'99 - Formal Methods, 1999

1997
Type-Checking Higher-Order Polymorphic Multi-Methods.
Proceedings of the Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

Rules for Abstraction.
Proceedings of the Advances in Computing Science, 1997

1996
On TLA as a logic.
Proceedings of the NATO Advanced Study Institute on Deductive Program Design, 1996

1995
Modular Description and Verification of Concurrent Objects.
Proceedings of the Object-Based Parallel and Distributed Computation, 1995

An Abstract Account of Composition.
Proceedings of the Mathematical Foundations of Computer Science 1995, 1995

Steam Boiler Control Specification Problem: A TLA Solution.
Proceedings of the Formal Methods for Industrial Applications, 1995

1994
Specifying and Verifying Fault-Tolerant Systems.
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.
Proceedings of the Formal Systems Specification, 1994

A TLA Solution to the RPC-Memory Specification Problem.
Proceedings of the Formal Systems Specification, 1994

1993
A Framework for Programming and Formalizing Concurrent Objects.
Proceedings of the SIGSOFT '93, 1993

Efficiently Executable Temporal Logic Programs.
Proceedings of the Executable Modal and Temporal Logics, 1993

1992
Temporal logic as a programming language.
PhD thesis, 1992

Decidability and incompleteness results for first-order temporal logics of linear time.
Journal of Applied Non-Classical Logics, 1992

1991
Temporal logic and recursion.
Fundam. Inform., 1991


  Loading...