# Stephan Merz - INRIA Nancy - Grand Est / LORIA

## Contact Details

NameStephan Merz |
||

AffiliationINRIA Nancy - Grand Est / LORIA |
||

Location |
||

## Pubs By Year |
||

## External Links |
||

## Pub CategoriesComputer 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

**Affiliations:**

^{1}VERIDIS,

^{2}VERIDIS

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:**

^{1}INRIA Nancy - Grand Est / LORIA,

^{2}INRIA Nancy - Grand Est / LORIA,

^{3}INRIA Nancy - Grand Est / LORIA

**Category:**Computer Science - Programming Languages

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

**Authors:**Damien Doligez

^{1}, Jael Kriener

^{2}, Leslie Lamport

^{3}, Tomer Libal

^{4}, Stephan Merz

^{5}

**Affiliations:**

^{1}INRIA Paris-Rocquencourt,

^{2}MSR - INRIA,

^{3}MSR - INRIA,

^{4}MSR - INRIA,

^{5}INRIA 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:**

^{1}INRIA Saclay - Ile de France,

^{2}INRIA Rocquencourt,

^{3}INRIA Lorraine,

^{4}INRIA 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

**Affiliations:**

^{1}INRIA Lorraine - LORIA,

^{2}INRIA Lorraine - LORIA

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:**

^{1}MRI,

^{2}INRIA Rocquencourt,

^{3}INRIA Lorraine - LORIA,

^{4}INRIA 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

**Affiliations:**

^{1}INRIA Lorraine - LORIA,

^{2}INRIA Lorraine - LORIA

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:**

^{1}IFI-LMU,

^{2}IFI-LMU,

^{3}INRIA 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