Probabilistic Programs (Seminar)

Seminar in Theoretical Computer Science, Winter Semester 2014/2015


  • 05.11.2014: Due to the Memorial Colloquium in commemoration of Prof. Dr. Berthold Vöcking on February 5 and 6 the dates of the seminar talks will be shifted to February 3 and 4.
  • 29.10.2014: The available topics are now online. Please find them below.
  • The kick-off meeting will take place on 16.10.2014 at 16:00h in the seminar room of our chair (room 4201b).
  • 25.6.2014: We are online!


16.10.2014, 16:00h Kick-off meeting at seminar room of i2
17.11.2014 Table of contents due
15.12.2014 Preliminary version of report due
05.01.2015 Final version of report due
19.01.2015 Preliminary version of slides due
26.01.2015 Final version of slides due
03.02.2015, 14:00h Seminar talks
04.02.2015, 09:00h Seminar talks


This seminar covers a variety of topics in the field of probabilistic programs. These kind of programs are of great importance e.g. in security, quantum computing, randomized algorithms and machine learning. A sample probabilistic program can be found here.

While probabilistic programs, for instance in their occurrence in security protocols, mostly consist of only a few lines of code, their underlying semantics is given by infinite systems such as Markov decision processes which makes the verification of most interesting properties very hard or even undecidable. In this seminar, we discuss the foundations of probabilistic programs, namely the underlying semantical models, as well as topics concerning the automated analysis of such programs.


Basic knowledge in the following areas is expected:

  • Semantics of programs
  • Probability theory
  • Automata theory
  • Mathematical logic
  • Previous knowledge in modelling probabilistic systems is helpful but not mandatory


No. Topic Supervisor Student Date
1 Expressing and Verifying Probabilistic Assertions. Sampson, Panchekha, Mytkowicz, McKinley, Grossman, Ceze. Katoen Hütter (paper, slides) 3.2.2015
2 Verifying Probabilistic Programs Using a Hoare Like Logic. den Hartog. Jansen Quatmann (paper, slides) 3.2.2015
3 Proof Rules for Probabilistic Loops. Carroll Morgan. Kaminski Korzeniewski (paper, slides) 3.2.2015
4 Expectation Invariants for Probabilistic Program Loops as Fixed Points. Chakarov, Sankaranarayanan. Katoen Florian (paper, slides) 3.2.2015
5 Proving Termination of Probabilistic Programs Using Patterns. Esparza, Gaiser, Kiefer. Jansen Westhofen (paper, slides) 4.2.2015
6 Probabilistic Program Analysis with Martingales. Chakarov, Sankaranarayanan. Olmedo Zwilling (paper, slides) 4.2.2015
7 Slicing Probabilistic Programs. Hur, Nori, Rajamani, Samuel. Olmedo Volk (paper, slides) 4.2.2015
8 The Satisfiability Problem for Probabilistic CTL. Brazdil, Forejt, Kretinsky, Kucera. Kaminski Berger (paper, slides) 4.2.2015

Additional Material


Registration to the seminar is handled between July 4 and 20, 2014, via the central online form at


Benjamin Kaminski, Nils Jansen, Federico Olmedo, Joost-Pieter Katoen