Probabilistic Termination

Title: Probabilistic Termination

Speaker: Holger Hermanns (Saarland University, Germany)          depend.cs.uni-sb.de/index.php?id=166

Time: 25th November 2014, 10:30

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

We propose a framework to prove almost sure termination for probabilistic programs with real valued variables. It is based on ranking supermartingales, a notion analogous to ranking functions on nonprobabilistic programs. The framework is proven sound and complete for a meaningful class of programs involving randomization and bounded nondeterminism. We complement this foundational insight by a practical proof methodology, based on sound conditions that enable compositional reasoning and are amenable to a direct implementation using modern theorem provers. This is integrated in a small dependent type system, to overcome the problem that lexicographic ranking functions fail when combined with randomization. Among others, this compositional methodology enables the verification of probabilistic programs outside the complete class that admits ranking supermartingales.

This is joint work with Luis Maria Ferrer Fioriti.

Holger Hermanns is a full professor at the Department of Computer Science at Saarland University, Saarbrücken, Germany, holding the chair for Dependable Systems and Software. He is former Dean of the Faculty of Mathematics and Computer Science at Saarland University, and has previously held positions at Universität Erlangen Nürnberg, Germany, at Universiteit Twente, the Netherlands, and at INRIA Grenoble Rhône-Alpes, France. His research interests include compositional modeling and verification of concurrent systems, resource-aware embedded systems, and performance and dependability evaluation of critical infrastructure. In these areas, Holger Hermanns has authored or co-authored more than 150 peer-reviewed scientific papers (ha-index 92). He has co-chaired the program committees of major international conferences such as TACAS 2006, CONCUR 2006, CAV 2007, and QEST 2012. He serves on the steering committees of ETAPS, TACAS and QEST. Holger Hermanns received the Dutch “Vernieuwingsimpuls” and the German “Preis des Fakultätentags Informatik” award, is elected member of Academia Europaea, coordinates the EU FP7 project MEALS, and holds several other national and European research grants.

The industrial impact of the research of Holger Hermanns in the area of quantitative correctness is exceptionally high. The largest chip manufacturer in Europe, ST-Microelectronics, is using tools co-developed with Prof. Hermanns, to find performance bottlenecks in their chip designs. HYDAC, a company specialized in hydraulic components, has cooperated with Prof. Hermanns to minimize the wear-out of a pump-storage system used for plastic injection molding. Other recent examples of very fruitful cooperations include work on wireless sensor

systems (with CHESS) and photovoltaic power generation forecasting (with Luxea GmbH and EnBW AG).