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

1. Static Analysis I
   • Literature: Static Analysis for Probabilistic Programs: Inferring whole Program Properties from Finitely many Paths. PLDI 2013.
     Sriram Sankaranarayanan, Aleksandar Chakarov, Sumit Gulwani.
   • Supervisor: Federico Olmedo
   • Student: —
2. Static Analysis II
   • Literature:  Synthesizing Probabilistic Invariants via Doob’s Decomposition.
     Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu.
   • Supervisor: Federico Olmedo
   • Student:
3. Relational Program Reasoning
   • Literature:  Relational Reasoning via Probabilistic Coupling. LPAR 2015.
     Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub.
   • Supervisor: Federico Olmedo
   • Student: —
4. 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: —
5. Runtime Analysis
   • Literature:  Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. ESOP 2016.
     Benjamin Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo.
   • Supervisor: Federico Olmedo
   • Student: —
6. 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
7. 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
8. 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
9. 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

10. Symmetry Reduction
    • Literature: Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives. ATVA 2006.
      Alastair F. Donaldson, Alice Miller.
    • Supervisor: Christian Dehnert
    • Student: —
11. Probabilistic Assertions
    • Literature: Expressing and Verifying Probabilistic Assertions. PLDI 2014.
      Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S. McKinley, Dan Grossman, Luis Ceze.
    • Supervisor: Christoph Matheja
    • Student: —
12. 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
13. 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>