Seminar in Theoretical Computer Science, Winter Semester 2014/2015

## News

- 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!

## Schedule

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 |

Overview

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.

## Prerequisites

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

## Topics

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

Registration to the seminar is handled between July 4 and 20, 2014, via the central online form at **www.graphics.rwth-aachen.de/apse.**

## Contact

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