Seminar in Theoretical CS, Winter Semester 2017/18

News

• 21.06.2017: Student-supervisor matching is online.
• 20.06.2017: Student-topic matching is online. Supervisor-student matching follows shortly.
• 16.08.2017: Dates are final.
• 16.08.2017: Tentative dates are online.
• 27.06.2017: We are online.

Dates & Deadlines

16.10.2017 at 14:00h in Room 4201b	Kick-off meeting
18.10.2017	Topic preferences due
23.10.2017	Topic notification
6.11.2017	Detailed outline due
13.11.2017	Consequenceless dropout date
4.12.2017	Seminar report due
18.12.2017	Seminar report camera-ready due
8.1.2018	Presentation slides due
22.1.2018	Presentation slides camera-ready due
5.2.2018 & 6.2.2018	Seminar talks

Note that the non-camera-ready versions of your report and your slides should be your final submission and the camera-ready versions should differ only with regard to minor remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting preliminary versions before the due dates.

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

Bachelor/Master Topics

1. MCMC sampling of probabilistic programs
   • Literature: Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel: A Provably Correct Sampler for Probabilistic Programs. FSTTCS 2015: 475-488
   • Supervisor: Christoph Matheja
   • Student: Simon Frenz
2. Slicing probabilistic programs
   • Literature: Torben Amtoft, Anindya Banerjee: A Theory of Slicing for Probabilistic Control Flow Graphs. FoSSaCS 2016: 180-196
   • Supervisor: Prof. Joost-Pieter Katoen
   • Student: Kevin Batz
3. Program analysis using martingales
   • Literature:  Aleksandar Chakarov, Sriram Sankaranarayanan: Probabilistic Program Analysis with Martingales. CAV 2013: 511-526
   • Supervisor: –
   • Student: –
4. Semantics of probabilistic programs
   • Literature: Sam Staton: Commutative Semantics for Probabilistic Programming. ESOP 2017: 855-879
   • Supervisor: Christoph Matheja
   • Student: Sezin Maden
5. Concurrent probabilistic programs
   • Literature: Vineet Gupta, Radha Jagadeesan, and Vijay A. Saraswat: Probabilistic concurrent constraint programming. CONCUR 1997:
     243–257
   • Supervisor: –
   • Student: –
6. Conditioning and recursion
   • Literature: Andreas Stuhlmüller and Noah D. Goodman. Reasoning about reasoning by nested conditioning: Modeling theory of mind with probabilistic programs. Cognitive Systems Research, 28:80–99, 2014
   • Supervisor: Prof. Joost-Pieter Katoen
   • Student: –
7. Probabilistic Kleene algebras
   • Literature: Annabelle McIver, Tahiry M. Rabehaja, Georg Struth: Probabilistic Concurrent Kleene Algebra. QAPL 2013: 97-115
   • Supervisor: Benjamin Kaminski
   • Student: –
8. Software-defined networks
   • Literature: Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, Alexandra Silva: Probabilistic NetKAT. ESOP 2016: 282-309
   • Supervisor: –
   • Student: –
9. Expected runtimes
   • Literature: Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. ESOP 2016
   • Supervisor: Christoph Matheja
   • Student: Christian Blumenthal
10. Computational hardness
    • Literature: Benjamin Lucien Kaminski & Joost-Pieter Katoen. On the Hardness of Almost-Sure Termination. MFCS 2015
    • Supervisor: Benjamin Kaminski
    • Student: David Herzkamp
11. Usefulness of non-termination
    • Literature: Thomas Icard. Beyond Almost-Sure Termination. CogSci 2017
    • Supervisor: Benjamin Kaminski
    • Student: –

Master Topics

12. Algorithmic analysis of termination
    • Literature: Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, Rouzbeh Hasheminezhad: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. POPL 2016: 327-342
    • Supervisor: Prof. Joost-Pieter Katoen
    • Student: Philipp Martin
13. Stochastic Invariants
    • Literature: Krishnendu Chatterjee, Petr Novotný, Dorde Zikelic. Stochastic Invariants for Probabilistic Termination. POPL 2017
    • Supervisor: –
    • Student: –
14. Lambda-calculus
    • Literature: Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak: A lambda-calculus foundation for universal probabilistic programming. ICFP 2016: 33-46
    • Supervisor: –
    • Student: –

Additional Material

Registration

Registration to the seminar is handled between Juni 30 and July 16, 2017, via the central online form.

Contact

Benjamin Kaminski, Christoph Matheja, Prof. Joost-Pieter Katoen