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.

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

DOIDownloadLinkBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica 56(3), pages 255-285, 2019.
DOIMaurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-based Conditioning of Probabilistic Data Integration (Best Paper Award). Proc. of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of LNAI, pages 290-305, Springer, 2018.
Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. A Program Analysis Perspective on Expected Sampling Times. Collected Abstracts of the 1st International Conference on Probabilistic Programming (PROBPROG 2018), 2018.
DOIBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM 65(5), pages 30:1-30:68, 2018.
DOIDownloadLinkKevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times.. Proc. of the 27th European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, pages 186-213, Springer, 2018.
DOIFederico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. ACM Transactions on Programming Languages and Systems (TOPLAS) 40(1), pages 4:1-4:50, 2018.
DOIAnnabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen. A New Proof Rule for Almost-Sure Termination. Proc. of the 45th Symposium on Principles of Programming Languages (POPL 2018), pages 33:1-33:28, 2018.
Show all