Verification of Probabilistic Programs


  • 2015-06-17: due to organisational tasks for the Sommerfest the lecture on 25th June is cancelled. A new lecture is schedule on 15th July (same time and room as usual).


In recent years, the relevance of probabilistic programs has increased at a remarkable pace. Nowadays they are pervasive in areas such as cryptography and machine learning and they have also a long tradition in the domain, for instance, of randomized algorithms. Due to their wide applicability, the verification of such probabilistic programs has become a central problem of active research. In this seminar we will overview how some well-known program verification techniques can be extended to deal with probabilistic programs. In particular, we will focus on extensions of fundamental and well-established techniques, which includes Hoare logics and weakest pre-condition calculus.


Federico Olmedo currently holds a Post-Doc position in the Software Modeling and Verification Group (i2) in the RWTH. Further information available on his personal webpage.


Any previous knowledge on program logics and semantics will be beneficial but it is not indispensable.

Schedule and Slides

The seminar comprises 6 presentations of 1h15 each, taking place in room 9U10 E3 from 16:30 to 17:45. 

No. Date Slides
1 3rd June Introduction
2 10th June Probabilistic Predicate Transformers I 
3 17th June Probabilistic Predicate Transformers II
4 1st July Probabilistic Hoare Logic
5 8th July Probabilistic Relational Hoare Logic I
6 15th July Probabilistic Relational Hoare Logic II