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

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. How long, O Bayesian network, will I sample thee?. Proc. of the 27th European Symposium on Programming (ESOP 2018), [to appear], Volume of LNCS, 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. PACMPL 2(Proc. of the 45th Symposium on Principles of Programming Languages (POPL 2018)), pages 33:1-33:28, 2018.
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.
Show all