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

2019
DOIDownloadLinkBenjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica 56(3), pages 255-285, 2019.
2018
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.
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.
DownloadLinkBenjamin 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.
2016
DOIDownloadLinkFederico 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.
DOIDownloadLinkJoost-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.
2015
DOIDownloadLinkJoost-Pieter Katoen. Probabilistic Programming: A True Challenge in Verification. 13th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), Volume of LNCS, pages 1–3, Springer-Verlag, 2015.
DownloadLinkNils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Probabilistic Programs - A Natural Model for Approximate Computations. Workshop on Approximate Computing (AC15), 2015.
DOIDownloadLinkMartin Fraenzle, Sebastian Gerwinn, Paul Kröger, Alessandro Abate, Joost-Pieter Katoen. Multi-Objective Parameter Synthesis in Probabilistic Hybrid Systems. 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Volume 9268 of LNCS, pages 93–107, Springer-Verlag, 2015.
DOIJoost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo. Understanding Probabilistic Programs. Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Volume 9360 of LNCS, pages 15-32, Springer, 2015.
DOIDownloadLinkBenjamin Lucien Kaminski, Joost-Pieter Katoen. On the Hardness of Almost-Sure Termination. Proc. of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS 2015), Part I, Volume 9234 of LNCS, pages 307-318, Springer, 2015.
DOIDownloadLinkChristian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, Erika Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. Proc. of the 27th Int. Conf. on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214–231, Springer, 2015.
DOIDownloadLinkTim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards. Proc. of the 20th Int. Symp. on Formal Methods (FM'15), Volume 9109 of LNCS, pages 435–452, Springer, 2015.
DOILinkLinkShashank Pathak, Erika Abraham, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models. Proc. of the 7th NASA Formal Methods Symp. (NFM'15), Volume 9058 of LNCS, pages 295–309, Springer, 2015.
DOIDownloadLinkRalf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata. Logical Methods in Computer Science (LMCS) 11(1:15), pages 1–23, 2015.
DownloadLinkBenjamin Lucien Kaminski. Analyzing Expected Outcomes and (Positive) Almost-Sure Termination of Probabilistic Programs is Hard. Proc. of the Young Researchers' Conference "Frontiers of Formal Methods" (FFM 2015), pages 179-184, Aachener Informatik Berichte, 2015.
DOIDownloadLinkNils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver. Conditioning in Probabilistic Programming. Proc. of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS 2015), ENTCS 319, pages 199-216, 2015.
2014
DownloadLinkJoost-Pieter Katoen. Model Checking Gigantic Markov Models. 12th International Conference on Software Engineering and Formal Methods (SEFM), Volume 8702 of LNCS, pages 1–2, , 2014.
DOIDownloadLinkNils Jansen, Ralf Wimmer, Erika Abraham, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster. Symbolic Counterexample Generation for Large Discrete-Time Markov Chains. Science of Computer Programming 91 (Part A), pages 90–114, 2014.
DOIDownloadLinkFriedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. Operational versus Weakest Pre-expectation Semantics for the Probabilistic Guarded Command Language. Performance Evaluation 73, pages 110–132, 2014.
DOIDownloadLinkJoost-Pieter Katoen, Lei Song, Lijun Zhang. Probably Safe or Live. Computer Science Logic and Logic in Computer Science (CSL-LICS), ACM, 2014.
DOIDownloadLinkTomas Brazdil, Stefan Kiefer, Antonín Kucera, Petr Novotny, Joost-Pieter Katoen. Zero-Reachability in Probabilistic Multi-Counter Automata. Computer Science Logic and Logic in Computer Science (CSL-LICS), ACM, 2014.
DOIDownloadLinkNils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. 11th Int. Conf. on Quantitative Evaluation of Systems (QEST'14), Volume 8657 of LNCS, pages 404–420, Springer, 2014.
DOIRalf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Linear-Time Probabilistic Verification. Theoretical Computer Science 549, pages 61–100, 2014.
DownloadLinkChristian Dehnert, Nils Jansen, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen. Fast Debugging of PRISM Models. Int. Symp. on Automated Technology for Verification and Analysis (ATVA'14), Volume 8837 of LNCS, pages 146–162, Springer, 2014.
2013
DownloadLinkNils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. Technical report at Cornell University number arXiv:1312.3979, 2013.
DOIDownloadLinkRalf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata. Proc. of the 10th Int. Conf. on Quantitative Evaluation of Systems (QEST'13), Volume 8054 of LNCS, pages 39–54, Springer-Verlag, 2013.
DownloadLinkJoost-Pieter Katoen. Model Checking Meets Probability: A Gentle Introduction. In , Engineering Dependable Software Systems, pages 177–205, Volume 34 of NATO Science for Peace and Security Series - D, 2013.
DownloadLinkFriedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. PRINSYS — on a Quest for Probabilistic Loop Invariants. 10th Int. Conf. on Quantitative Evaluation of Systems (QEST'13), Volume 8054 of LNCS, pages 172–187, Springer, 2013.
2012
DownloadLinkFriedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. Quantitative Evaluation of Systems (QEST), IEEE CS Press, 2012.
2011
LinkLinkHongfei Fu, Joost-Pieter Katoen. Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems. Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Volume 13 of LIPIcs, pages 445–456, Schloss Dagstuhl, 2011.
2010
DownloadLinkJoost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, Carroll Morgan. Linear-Invariant Generation for Probabilistic Programs. Static Analysis Symposium (SAS), Volume 6337 of LNCS, pages 390–406, Springer-Verlag, 2010.