Stephan Merz - INRIA Nancy - Grand Est / LORIA

Stephan Merz
Are you Stephan Merz?

Claim your profile, edit publications, add additional information:

Contact Details

Stephan Merz
INRIA Nancy - Grand Est / LORIA

Pubs By Year

External Links

Pub Categories

Computer Science - Logic in Computer Science (9)
Computer Science - Cryptography and Security (1)
Computer Science - Programming Languages (1)
Computer Science - Software Engineering (1)

Publications Authored By Stephan Merz


With state-based methods, checking that an implementation satisfies a higher-level specification requires describing how the higher-level concepts in the specification are represented by the lower-level data structures of the implementation. This approach was first proposed in the domain of sequential systems by Hoare in 1972. Hoare called the description an abstraction function. Read More

We present an encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This translation is the main component of a back-end prover based on SMT solvers in the TLA+ Proof System. Read More

Affiliations: 1INRIA Nancy - Grand Est / LORIA, 2INRIA Nancy - Grand Est / LORIA, 3INRIA Nancy - Grand Est / LORIA

Avoiding access conflicts is a major challenge in the design of multi-threaded programs. In the context of real-time systems, the absence of conflicts can be guaranteed by ensuring that no two potentially conflicting accesses are ever scheduled concurrently.In this paper, we analyze programs that carry time annotations specifying the time for executing each statement. Read More

Affiliations: 1INRIA Paris-Rocquencourt, 2MSR - INRIA, 3MSR - INRIA, 4MSR - INRIA, 5INRIA Nancy - Grand Est / LORIA

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic. Read More

TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs. Read More

Affiliations: 1INRIA Saclay - Ile de France, 2INRIA Rocquencourt, 3INRIA Lorraine, 4INRIA Lorraine

TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. Read More

Modern functional-logic programming languages like Toy or Curry feature non-strict non-deterministic functions that behave under call-time choice semantics. A standard formulation for this semantics is the CRWL logic, that specifies a proof calculus for computing the set of possible results for each expression. In this paper we present a formalization of that calculus in the Isabelle/HOL proof assistant. Read More

Affiliations: 1MRI, 2INRIA Rocquencourt, 3INRIA Lorraine - LORIA, 4INRIA Lorraine - LORIA

We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Read More


We consider the interpretations of notions of access control (permissions, interdictions, obligations, and user rights) as run-time properties of information systems specified as event systems with fairness. We give proof rules for verifying that an access control policy is enforced in a system, and consider preservation of access control by refinement of event systems. In particular, refinement of user rights is non-trivial; we propose to combine low-level user rights and system obligations to implement high-level user rights. Read More

Affiliations: 1IFI-LMU, 2IFI-LMU, 3INRIA Lorraine - LORIA

We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized B\"{u}chi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized B\"{u}chi automaton, and a variant of Tarjan's algorithm is used to decide the existence of an accepting run of the product of the transition system and the automaton. Because we avoid an explicit construction of the B\"{u}chi automaton, our approach can yield significant improvements in runtime and memory, for large LTL formulas. Read More