Keynote talk II

II- Probabilistic Programming: Semantics, Termination, and Run Time Analysis

katoen Joost-Pieter Katoen
RWTH Aachen University, Germany

Joost-Pieter Katoen is a distinguished professor in Software Modelling and Verification at RWTH Aachen University, Germany. He is part-time professor at the University of Twente, The Netherlands, steering committee chair of ETAPS, and member of the Academia Europaea. His research interests include formal semantics, concurrency theory, computer-aided verification, and probabilistic models.

Probabilistic programs are used in different application areas, ranging from machine learning to security, software-defined networking and quantum computing.  In this talk, I’ll discuss some semantic issues of probabilistic programming languages and present several nuances of termination: whereas ordinary program termination is about whether a program has an infinite run or not, for probabilistic programs this is much more delicate.  I’ll show that almost-sure termination — does a program terminate with probability one? — is « more undecidable » than ordinary termination, and discuss that a program may almost surely terminate although this may on average take an infinite amount of steps. Finally, I’ll propose a variant of Dijkstra’s wp-calculus to establish the expected run-time of a probabilistic program.


These are firm deadlines

January 12, 2016

Abstract submission deadline

January 23, 2016

Paper submission deadline

March 15, 2016

Acceptance notification

April 05, 2016

Camera ready copy due



The proceedings of the conference will be published in Springer’s Lecture Notes in Computer Science

Partners & Sponsors