News

• 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).

Abstract

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.

Lecturer

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.

Pre-requisites

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