FRAPPANT’s objective is to enable predictable probabilistic programming by developing unique, advanced formal verification techniques.

ERC Advanced Grant 2017 (787914). Project duration: 1.11.2018 to 31.10.2024. See also the CORDIS fact sheet on FRAPPANT and the RWTH press release.
Researchers. Joost-Pieter Katoen, Kevin Batz, Lutz Klinkenberg, Bahare Salmani, Philipp Schroer.
Abstract
Probabilistic programs describe recipes on how to infer statistical conclusions about data from a complex mixture of uncertain data and real-world observations. They can represent probabilistic graphical models far beyond the capabilities of Bayesian networks and are expected to have a major impact on machine intelligence.
Probabilistic programs are ubiquitous. They steer autonomous robots and self-driving cars, are key to describe security mechanisms, naturally code up randomised algorithms for solving NP-hard problems, and are rapidly encroaching AI. Probabilistic programming aims to make probabilistic modeling and machine learning accessible to the programmer.
Probabilistic programs, though typically relatively small in size, are hard to grasp, let alone automatically checkable. Are they doing the right thing? What’s their precision? These questions are notoriously hard — even the most elementary question “does a program halt with probability one?” is “more undecidable” than the halting problem — and can (if at all) be answered with statistical evidence only. Bugs thus easily occur. Hard guarantees are called for. The objective of this project is to enable predictable probabilistic programming. We do so by developing formal verification techniques.
Whereas program correctness is pivotal in computer science, the formal verification of probabilistic programs is in its infancy. The project aims to fill this barren landscape by developing program analysis techniques, leveraging model checking, deductive verification, and static analysis. Challenging problems such as checking program equivalence, loop-invariant and parameter synthesis, program repair, program robustness and exact inference using weakest precondition reasoning will be tackled. The techniques will be evaluated in the context of probabilistic graphical models, randomised algorithms, and autonomous robots.
FRAPPANT will spearhead formally verifiable probabilistic programming.
Thesis Projects, Lectures, and Seminars
If you are interested in working on this project as a thesis or Hiwi student, contact one of our researchers on the project. We always have interesting topics available related to this project.
We also provide a recurring lecture series on probabilistic programs. For example, check out the WS 2022/23 lecture page. Furthermore, our seminars regularly deal with topics related to FRAPPANT. Head over to our teaching page for more information.
Our Publications Related to FRAPPANT
2023 | |
---|---|
![]() |
Kevin Batz, Mingshuai Chen, Sebastian Junges, , Joost-Pieter Katoen, . Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, Tools and Algorithms for the Construction and Analysis of Systems, Volume 13994 of LNCS, 2023. |
![]() |
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 2023. |
2022 | |
![]() |
Mingshuai Chen, Bai Xue, , Joost-Pieter Katoen. Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming, Information and computation 289 (A), pages 104965, Elsevier, 2022. | ,
2021 | |
![]() ![]() |
Matthias Volk, , Joost-Pieter Katoen, . Synthesizing optimal bias in randomized self-stabilization, Distributed computing 35 (1), pages 37-57, Springer, 2021. |
![]() ![]() |
Bahare Salmani Barzoki, Joost-Pieter Katoen. Fine-Tuning the Odds in Bayesian Networks, European Conference on Symbolic and Quantitative Approaches with Uncertainty (ECSQARU), Volume 12897 of LNCS, 268-283, Springer, 2021. |
![]() ![]() |
Hans Christian Hensel, , Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, International journal on software tools for technology transfer 24 (4), pages 589-610, Springer, 2021. |
![]() |
Joshua Moerman. Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata, 36. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), ACM Conferences, [1]-13, Association for Computing Machinery, 2021. | , ,
![]() ![]() |
Kevin Batz, Mingshuai Chen, , Joost-Pieter Katoen, , Philipp Schröer. Latticed $k$-Induction with an Application to Probabilistic Programs, 33. International Conference on Computer-Aided Verification (CAV 2021), Volume 12760 of LNCS, 524-549, Springer, 2021. |
![]() ![]() |
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming, 33. International Conference on Computer-Aided Verification (CAV 2021), Volume 12759, Theoretical Computer Science and General Issues of LNCS, 443-466, Springer, 2021. |
![]() ![]() |
Joost-Pieter Katoen, . A pre-expectation calculus for probabilistic sensitivity, Proceedings of the ACM on programming languages 5 (POPL), pages 52, Association for Computing Machinery, 2021. | , , , ,
![]() ![]() |
Joshua Moerman. Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata, 16 Seiten, 2021. https://arxiv.org/abs/2104.02438 | , ,
![]() ![]() |
Kevin Batz, , Joost-Pieter Katoen, . Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning, Proceedings of the ACM on programming languages 5, pages 39, ACM, 2021. |
![]() |
Joost-Pieter Katoen, , Tobias Winkler. The complexity of reachability in parametric Markov decision processes, Journal of computer and system sciences 119, pages 183-210, Elsevier, 2021. | ,
![]() ![]() |
Joost-Pieter Katoen (ed), . Foundations of probabilistic programming, xiv, 568 Seiten : Illustrationen, Cambridge University Press, 2021. | ,
![]() |
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 30. International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020), Volume 12561 of Theoretical Computer Science and General Issues, 231-248, Springer, 2021. |
2020 | |
![]() ![]() |
Bahare Salmani Barzoki, Joost-Pieter Katoen. Bayesian Inference by Symbolic Model Checking, 17. International Conference on Quantitative Evaluation of SysTems (QEST 2020), Volume 12289 of LNCS, 115-133, Springer, 2020. |
![]() ![]() |
Mingshuai Chen, , , , . Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control, Acta informatica 58 (5), pages 497-528, Springer, 2020. |
![]() ![]() |
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3: Property Directed Reachability for MDPs, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 512-538, Springer, 2020. |
![]() |
Marcin Szymczak, Joost-Pieter Katoen. Weakest Preexpectation Semantics for Bayesian Inference: Conditioning, Continuous Distributions and Divergence, 5. School on Engineering Trustworthy Software Systems (SETSS 2019), Volume 12154 of LNCS, 44-121, Springer, 2020. |
|
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 2020. https://arxiv.org/abs/2007.06327 |
![]() |
Joshua Moerman, Matteo Sammartino. Residual Nominal Automata, 31. International Conference on Concurrency Theory (CONCUR 2020), Volume 171 of Leibniz international proceedings in informatics, 44:1-44:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2020. |
![]() ![]() |
Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan. Unbounded-Time Safety Verification of Stochastic Differential Dynamics, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 327-348, Springer, 2020. |
|
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer. PrIC3: Property Directed Reachability for MDPs, 2020. https://arxiv.org/abs/2004.14835 |
![]() ![]() |
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, . Learning One-Clock Timed Automata, 26. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078, Theoretical Computer Science and General Issues of LNCS, 444-462, Springer, 2020. |
![]() ![]() |
Joshua Moerman, . Separation and Renaming in Nominal Sets, 28. EACSL Annual Conference on Computer Science Logic (CSL 2020), Volume 152 of Leibniz international proceedings in informatics, 31:1-31:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, January, 2020. |
2019 | |
![]() |
Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches, 3. World Congress on Formal Methods (FM 2019), Volume 11800 of LNCS, 101-120, Springer, 2019. | ,
|
Joshua Moerman, . Separation and Renaming in Nominal Sets, 23 Seiten, 2019. https://arxiv.org/abs/1906.00763 |
![]() ![]() |
Joshua Moerman, . Residual Nominal Automata, 25 Seiten, 2019. https://arxiv.org/abs/1910.11666 |
![]() |
Hans Christian Dehnert, , Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped, Volume 11500 of LNCS, 107-125, Springer, 2019. | ,
![]() ![]() |
Tim Quatmann, Enno Ruijters. The Quantitative Verification Benchmark Set, 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 11427 of LNCS, 344-350, Springer, 2019. | , , ,
![]() ![]() |
Benjamin Lucien Kaminski. Advanced weakest precondition calculi for probabilistic programs, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xiv, 363 Seiten) : Illustrationen, Diagramme, 2019. |
![]() ![]() |
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs, Proceedings of the ACM on programming languages 3 (POPL), pages 34, ACM, 2019. |
2018 | |
![]() |
Peter Burggräf, Matthias Dannapfel, Hanno Arnd Voet, , Jerome Uelpenich, . Digital Transformation of Lean Production: Systematic Approach for the Determination of Digitally Pervasive Value Chains, International Journal on Operations Management and Industrial Engineering 17 (10), pages 671-680, Apprimus Verlag, 2018. |