Seminar in Theoretical CS, Summer Semester 2016

### News

- 19.01.2016: we are online
- 23.02.2016: the course kick-off meeting will take place on April 13th at 14:30 in room 9U10 (E3).
- 08.03.2016: the course topics are already available
- 14.04.2016: topic-student assignment is already available

### Deadlines

13th April | Kick-off meeting |

23th May | Seminar report due |

19th June | Presentation slides due |

29-30th June | Seminar talks |

### Overview

This seminar covers a variety of topics in the field of probabilistic programs. Roughly speaking, probabilistic programs are like ordinary programs, with an extra feature: the ability to make some sort of probabilistic choice. Here we show how one can exploit this feature to model, for instance, a duel between two cowboys. These kind of programs are of great importance due to their wide applicability scope, which includes, amongst others, security, quantum computing, randomized algorithms and machine learning.

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:

#### Master Students

- Static Analysis I
- Static Analysis II
- Relational Program Reasoning
- Deductive Verification
**Literature**: A Program Logic for Union Bounds.

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.**Supervisor**: Federico Olmedo**Student**: —

- Runtime Analysis
- Game-Based Abstraction Refinement
**Literature**: Abstraction Refinement for Probabilistic Software. VMCAI 2009.

Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, David Parker**Supervisor**: Christian Dehnert**Student**: Sascha Kurowski

- Probabilistic CTL
**Literature**: Probabilistic CTL* : The Deductive Way. Rayna Dimitrova , Luis Marıa Ferrer Fioriti, Holger Hermanns , Rupak Majumdar**Supervisor**: Christoph Matheja**Student**: Lea Hiendl

- Analysis of Probabilistic Pushdown Automata
**Literature**: Analyzing Probabilistic Pushdown Automata. FMSD 2013.

Tomáš Brázdil, Javier Esparza, Stefan Kiefer, Antonín Kučera**Supervisor**: Sebastian Junges**Student**: Justin Winkens

- Kleene Algebra with Tests
**Literature:**Probabilistic NetKAT. ESOP 2016.

Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, Alexandra Silva**Supervisor:**Benjamin Kaminski**Student:**—

#### Bachelor Students

- Symmetry Reduction
- Probabilistic Assertions
- Bringing Probabilistic Programming to MS Excel
**Literature**: Probabilistic Programming as Spreadsheet Queries.

Andrew D. Gordon, Claudio Russo, Marcin Szymczak, Johannes Borgstrom, Nicolas Rolland, Thore Graepel, and Daniel Tarlow**Supervisor**: Sebastian Junges**Student**: Tobias Standop

- Proving Almost-Sure Termination
**Literature:**Proving Termination of Probabilistic Programs Using Patterns. CAV 2012.

Javier Esparza, Andreas Gaiser, Stefan Kiefer**Supervisor:**Benjamin Kaminski**Student:**Georg Clegg

### Schedule for Seminar Talks

The seminar talks will take place on June 30th, in the chair’s seminar room (E1, room 4201b). Detailed schedule is given below.

10:15 | Justin Winkens | Analysis of Probabilistic Pushdown Automata |

11:00 | Georg Clegg | |

13:00 | Kurowski Sascha | Abstraction Refinement for Probabilistic Software |

13:45 | Lea Hiendl | PCTL* – The Deductive Way |

14:30 | Tobias Standop | Probabilistic Programming as Spreadsheet Queries |

### Additional Material

### Registration

Registration to the seminar is handled between January 14 and 27, 2016, via the central online form**.**

### Contact

Federico Olmedo <federico.olmedo at cs.rwth-aachen.de>