A Proof Rule for Multi-Threaded Programs

A modular proof rule for the verification of temporal safety and liveness properties of multi-threaded programs, and how this rule can be transformed into an automatic method.

Joint work with Ashutosh Gupta and Corneliu Popeea.

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.