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

The APPA project, funded by the Excellence Initiative of the German federal and state government, aims at developing techniques for the automated analysis of probabilistic programs. These kind of programs are of great importance in fields such as security, quantum computing, randomized algorithms and machine learning, where Bayesian inference is needed for the analysis.

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 certain probabilities very hard or even undecidable. In the scope of this project, we explore the possibilities of automated analysis techniques given the fact that we have to handle infinite domains in combination with arbitrary parameters. This is done by means of identifying reasonable sub-classes, where results on the underlying semantics can be used, as well as by developing new techniques.

A sample probabilistic program can be found here.

Theses
If you are interested in writing your thesis (Bachelor or Master) in this highly active field, please contact one of the participating persons mentioned above. For example, we offer the following topics:

• Modeling and analysis of probabilistic programs, which concerns the modeling of well-known stochastic processes as probabilistic programs and their evaluation. The results will be used to determine certain difficulties and properties of these programs in order to devise new analysis techniques.