APPA – Automated Probabilistic Program Analysis

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.

Publications related to APPA

2017
DOIBenjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Proc. of the 32nd Annual Symposium on Logic in Computer Science (LICS 2017), pages 1-12, IEEE, 2017.
DownloadBenjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Collected Abstracts of the 2nd Workshop on Probabilistic Programming Semantics (PPS 2017), 2017.
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. In , ACM Transactions on Programming Languages and Systems (TOPLAS), [to appear], 2017.
2016
DownloadFederico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs. Proc. of the 31st Annual Symposium on Logic in Computer Science (LICS 2016), pages 672-681, ACM, 2016.
DownloadJoost-Pieter Katoen. The Probabilistic Model Checking Landscape. Proc. of Logic in Computer Science (LICS), pages 31-46, ACM, 2016.
DOIBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (EATCS Best Paper Award). Proc. of the 25th European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, pages 364 - 389, Springer, 2016.
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo. On the Semantic Intricacies of Conditioning. Collected Abstracts of the 1st Workshop on Probabilistic Programming Semantics (PPS 2016), 2016.
Show all