Transition Invariants

  • Andrey Rybalchenko | Max-Planck-Institut fuer Informatik, Saarbruecken

Proof rules for the temporal verification of concurrent programs rely on auxiliary assertions. We propose a (sound and relatively complete) proof rule whose auxiliary assertions are transition invariants. A transition invariant of a program is a binary relation over program states that contains the transitive closure of the transition relation of the program. A transition invariant is disjunctively well-founded if it is a finite union of well-founded relations. We characterize the validity of a liveness property by the existence of a disjunctively well-founded transition invariant.

Speaker Details

Andrey Rybalchenko is researcher at Max Planck Institute for Computer Science in Saarbruecken and at Ecole Polytechnique Federale de Lausanne. He holds Dipl.-Inf. (2002) and Dr.-Ing. (summa cum laude, 2005) degrees from the University of Saarland, Germany. Andrey’s research interests focus on automated methods and tools for formal software verification, ranging from the design of program analysis methods to the development of algorithms for symbolic computation and automated deduction. Andrey’s doctoral research revolutionized verification of liveness properties for software systems by introducing “transition invariants”. Jointly with Microsoft Research, Andrey developed the Terminator tool, which is the first tool to perform automatic verification of liveness properties for software. He is also developing the ARMC tool for automatically proving safety properties of complex infinite state systems, which has been successfully applied for the verification of safety critical parts of the European Train Control System. Andrey is a recipient of Guenther Hotz medal (2002) from the University of Saarland and Otto Hahn medal (2005) from the Max Planck Society.

Watch Next