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