Conferences - Seminars

  Thursday 22 February 2018 11:15 - 12:15 BC410

Auxiliary variables revisited

By Stephan Merz, Inria Nancy (joint work with Leslie Lamport)

Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal
description of the implementation without changing its semantics—that is, the set of behaviors that it describes. I will present rules for introducing history, prophecy, and stuttering variables and discuss completeness results for these rules.

Stephan Merz is a researcher at Inria Nancy and head of the VeriDis research group interested in techniques of computer-aided deduction and their application to distributed algorithms and systems. He obtained his PhD and habilitation degrees at the University of Munich, working on temporal logic and formal methods for the specification and verification of computer systems.

More information

Contact Host: Laboratory for Automated Reasoning and Analysis,

Accessibility General public

Admittance Free