• Browsing: »
  • Home
  • »Research
  • »Projects
  • »FRAPPANT – Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation

FRAPPANT – Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation

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

erc logo

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. Former members: Jushua Moermann, Mingshuai Chen, Benjamin Kaminski, Marcin Szymczak.

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.

Recent Research Highlights

To give an overview of our work, each of our current researchers presents highlights one of their recent publications.

Kevin Batz: Probabilistic program verification via inductive synthesis of inductive invariants

Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We have developed a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.

Bahare Salmani: Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks

As a FRAPPANT member, I work on Bayesian Networks (BNs) and how they relate to probabilistic model checking. I’ve focused my research on probabilistic (and symbolic) inference, sensitivity analysis, and parameter tuning on BNs. Our latest paper entitled “Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks” has been recently accepted for presentation at IJCAI 2023 (the 32nd Int. Joint Conf. on Artificial Intelligence) in Macao. Out of 4566 full-paper submissions, about 15% have been accepted. The paper gives an algorithm for estimating the sensitivity of a given fully-specified Bayesian network to small perturbations in the values of local conditional probabilities.

Philipp Schroer: Building an Infrastructure for Probabilistic Program Verification

We are developing Caesar, a deductive verifier for probabilistic programs. It is based on our verification infrastructure for probabilistic programs, similar to a probabilistic version of Boogie. Our work includes an intermediate verification language called HeyVL and a real-valued logic called HeyLo. This allows us to generate verification conditions that prove a program’s correctness. Our focus is on measuring properties like expected outcomes and termination probabilities, so we use a real-valued approach instead of the usual Boolean logic. Our IVL adapts standard verification elements to handle quantitative aspects and uses weakest preexpectation-style semantics to generate verification conditions. Our SMT-based implementation Caesar enables us to automatically verify a wide range of benchmarks.

Caesar has a website where you can download the tool and find its documentation, including a tutorial-style guide. It is developed as an open-source project on Github. A paper on HeyVL and Caesar was published at OOPSLA 2023 and there’s an extended version available on arxiv.

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.

List of Publications Related to FRAPPANT

2025
DOI [bibtex]
@inbook{JPMFP2025,
title = {J-P: MDP. FP. PP},
author = {Kevin Batz and Benjamin Lucien Kaminski and Christoph Matheja and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {15260},
pages = {255-302},
type = {Book Chapter},
year = {2025},
doi = {10.1007/978-3-031-75783-9_11},
url = { https://publications.rwth-aachen.de/record/999819},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler. J-P: MDP. FP. PP, Volume 15260 of LNCS, 255-302, Springer, 2025.
DOI [bibtex]
@inbook{SQIFPP2025,
title = {Symbolic Quantitative Information Flow for Probabilistic Programs},
author = {Philipp Schröer and Francesca Randone and Raúl Pardo and Andrzej Wa̧sowski},
publisher = {Springer},
booktitle = {LNCS},
volume = {15260},
pages = {128-154},
type = {Book Chapter},
year = {2025},
doi = {10.1007/978-3-031-75783-9_6},
url = { https://publications.rwth-aachen.de/record/998367},
}×
[issue] 		Philipp Schröer, Francesca Randone, Raúl Pardo, Andrzej Wa̧sowski. Symbolic Quantitative Information Flow for Probabilistic Programs, Volume 15260 of LNCS, 128-154, Springer, 2025.
2024
DOI fulltext PDF [bibtex]
@phdthesis{A2024,
title = {Automated deductive verification of probabilistic programs},
author = {Kevin Batz},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {PhD Thesis},
year = {2024},
doi = {10.18154/RWTH-2025-00473},
url = { https://publications.rwth-aachen.de/record/1002329},
}×
[issue] 		Kevin Batz. Automated deductive verification of probabilistic programs, PhD Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@phdthesis{PB2024,
title = {Probabilistic model checking and parameter tuning for Bayesian networks},
author = {Bahare Salmani Barzoki},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {PhD Thesis},
year = {2024},
doi = {10.18154/RWTH-2025-00411},
url = { https://publications.rwth-aachen.de/record/1002228},
}×
[issue] 		Bahare Salmani Barzoki. Probabilistic model checking and parameter tuning for Bayesian networks, PhD Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@article{EBILPPGF2024,
title = {Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions},
author = {Lutz Klinkenberg and Christian Blumenthal and Mingshuai Chen and Darion Haase and Joost-Pieter Katoen},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {8(OOPSLA1)},
pages = {pages 127},
type = {Journal Article},
year = {2024},
doi = {10.1145/3649844},
url = { https://publications.rwth-aachen.de/record/986464},
}×
[issue] 		Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions, Proceedings of the ACM on programming languages 8 (OOPSLA1), pages 127, ACM, 2024.
DOI fulltext PDF [bibtex]
@article{PSSRNPP2024,
title = {Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs},
author = {Kevin Batz and Tom Jannik Biskup and Joost-Pieter Katoen and Tobias Winkler},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {8},
pages = {pages 93},
type = {Journal Article},
year = {2024},
doi = {10.1145/3632935},
url = { https://publications.rwth-aachen.de/record/979194},
}×
[issue] 		Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs, Proceedings of the ACM on programming languages 8, pages 93, ACM, 2024.
2023
DOI arXiv:2307.07314 [bibtex]
@unpublished{EBILPPGF2023,
title = {Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions},
author = {Lutz Klinkenberg and Christian Blumenthal and Mingshuai Chen and Darion Haase and Joost-Pieter Katoen},
pages = {54 Seiten},
type = {Preprint},
year = {2023},
doi = {10.48550/ARXIV.2307.07314},
url = { https://arxiv.org/abs/2307.07314},
}×
[issue] 		Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions, 54 Seiten, 2023. https://arxiv.org/abs/2307.07314
DOI [bibtex]
@conference{FCMVPBN2023,
title = {Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks},
author = {Bahare Salmani Barzoki and Joost-Pieter Katoen},
publisher = {International Joint Conferences on Artificial Intelligence},
type = {Conference Paper},
year = {2023},
doi = {10.24963/ijcai.2023/635},
url = { https://publications.rwth-aachen.de/record/990327},
}×
[issue] 		Bahare Salmani Barzoki, Joost-Pieter Katoen. Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks, 32. International Joint Conference on Artificial Intelligence (IJCAI 2023), International Joint Conferences on Artificial Intelligence, 2023.
DOI arXiv:2309.07781 fulltext PDF [bibtex]
@unpublished{ADVIPPEV2023,
title = {A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)},
author = {Philipp Schroer and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
pages = {[1]-48},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2309.07781},
url = { https://arxiv.org/abs/2309.07781},
}×
[issue] 		Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version), [1]-48, 2023. https://arxiv.org/abs/2309.07781
DOI fulltext PDF [bibtex]
@article{ADVIPP2023,
title = {A Deductive Verification Infrastructure for Probabilistic Programs},
author = {Philipp Schroer and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {7(OOPSLA2)},
pages = {pages 294},
type = {Journal Article},
year = {2023},
doi = {10.1145/3622870},
url = { https://publications.rwth-aachen.de/record/973293},
}×
[issue] 		Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA2), pages 294, ACM, 2023.
DOI [bibtex]
@conference{OCERTPPA2023,
title = {On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata},
author = {Tobias Winkler and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {13 Seiten},
type = {Conference Paper},
year = {2023},
doi = {10.1109/LICS56636.2023.10175714},
url = { https://publications.rwth-aachen.de/record/972664},
}×
[issue] 		Tobias Winkler, Joost-Pieter Katoen. On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata, 38. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), 13 Seiten, IEEE, 2023.
DOI fulltext PDF [bibtex]
@conference{CPPAOVI2023,
title = {Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration},
author = {Tobias Winkler and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13994},
pages = {391-409},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30820-8_24},
url = { https://publications.rwth-aachen.de/record/972636},
}×
[issue] 		Tobias Winkler, Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 391-409, Springer, 2023.
DOI fulltext PDF [bibtex]
@conference{SESPSP2023,
title = {Search and Explore: Symbiotic Policy Synthesis in POMDPs},
author = {Roman Andriushchenko and Alexander Nikolai Bork and Milan Češka and Sebastian Junges and Joost-Pieter Katoen and Filip Macák},
publisher = {Springer},
booktitle = {LNCS},
volume = {13966},
pages = {113-135},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-37709-9_6},
url = { https://publications.rwth-aachen.de/record/968844},
}×
[issue] 		Roman Andriushchenko, Alexander Nikolai Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Filip Macák. Search and Explore: Symbiotic Policy Synthesis in POMDPs, 35. International Conference on Computer-Aided Verification (CAV 2023), Volume 13966 of LNCS, 113-135, Springer, 2023.
DOI fulltext PDF [bibtex]
@conference{PPVISII2023,
title = {Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants},
author = {Kevin Batz and Mingshuai Chen and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {13994},
pages = {410-429},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30820-8_25},
url = { https://publications.rwth-aachen.de/record/957952},
}×
[issue] 		Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 410-429, Springer, 2023.
DOI arXiv:2302.00513 fulltext PDF [bibtex]
@unpublished{EPIUGF2023,
title = {Exact Probabilistic Inference Using Generating Functions},
author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen},
pages = {3 Seiten},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2302.00513},
url = { https://arxiv.org/abs/2302.00513},
}×
[issue] 		Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 3 Seiten, 2023. https://arxiv.org/abs/2302.00513
2022
DOI [bibtex]
@article{ES2022,
title = {Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Information and computation},
volume = {289(A)},
pages = {pages 104965},
type = {Journal Article},
year = {2022},
doi = {10.1016/j.ic.2022.104965},
url = { https://publications.rwth-aachen.de/record/853946},
}×
[issue] 		Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, 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
DOI fulltext PDF [bibtex]
@article{S2021,
title = {Synthesizing optimal bias in randomized self-stabilization},
author = {Matthias Volk and Borzoo Bonakdarpour and Joost-Pieter Katoen and Saba Aflaki},
publisher = {Springer},
journal = {Distributed computing},
volume = {35(1)},
pages = {pages 37-57},
type = {Journal Article},
year = {2021},
doi = {10.1007/s00446-021-00408-4},
url = { https://publications.rwth-aachen.de/record/835189},
}×
[issue] 		Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Saba Aflaki. Synthesizing optimal bias in randomized self-stabilization, Distributed computing 35 (1), pages 37-57, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{FTOBN2021,
title = {Fine-Tuning the Odds in Bayesian Networks},
author = {Bahare Salmani Barzoki and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12897},
pages = {268-283},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-86772-0_20},
url = { https://publications.rwth-aachen.de/record/828686},
}×
[issue] 		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.
DOI fulltext PDF [bibtex]
@article{TS2021,
title = {The probabilistic model checker STORM},
author = {Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {24(4)},
pages = {pages 589-610},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10009-021-00633-z},
url = { https://publications.rwth-aachen.de/record/822059},
}×
[issue] 		Hans Christian Hensel, Sebastian Junges, 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.
DOI [bibtex]
@conference{OFDVSWRA2021,
title = {Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata},
author = {Mikolaj Bojanczyk and Bartek Klin and Joshua Moerman},
publisher = {Association for Computing Machinery},
booktitle = {ACM Conferences},
pages = {[1]-13},
type = {Conference Paper},
year = {2021},
doi = {10.1109/LICS52264.2021.9470634},
url = { https://publications.rwth-aachen.de/record/847230},
}×
[issue] 		Mikolaj Bojanczyk, Bartek Klin, 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.
DOI fulltext PDF [bibtex]
@conference{LIAPP2021,
title = {Latticed $k$-Induction with an Application to Probabilistic Programs},
author = {Kevin Batz and Mingshuai Chen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12760},
pages = {524-549},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81688-9_25},
url = { https://publications.rwth-aachen.de/record/822587},
}×
[issue] 		Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, 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.
DOI fulltext PDF [bibtex]
@conference{SIBCDCP2021,
title = {Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12759, Theoretical Computer Science and General Issues},
pages = {443-466},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81685-8_21},
url = { https://publications.rwth-aachen.de/record/822586},
}×
[issue] 		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.
DOI fulltext PDF [bibtex]
@article{A2021,
title = {A pre-expectation calculus for probabilistic sensitivity},
author = {Alejandro Aguirre and Gilles Barthe and Justin Hsu and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Association for Computing Machinery},
journal = {Proceedings of the ACM on programming languages},
volume = {5(POPL)},
pages = {pages 52},
type = {Journal Article},
year = {2021},
doi = {10.1145/3434333},
url = { https://publications.rwth-aachen.de/record/819375},
}×
[issue] 		Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A pre-expectation calculus for probabilistic sensitivity, Proceedings of the ACM on programming languages 5 (POPL), pages 52, Association for Computing Machinery, 2021.
DOI arXiv:2104.02438 fulltext PDF [bibtex]
@unpublished{OFDVSWRA2021,
title = {Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata},
author = {Mikołaj Bojańczyk and Bartek Klin and Joshua Moerman},
pages = {16 Seiten},
type = {Preprint},
year = {2021},
doi = {10.48550/ARXIV.2104.02438},
url = { https://arxiv.org/abs/2104.02438},
}×
[issue] 		Mikołaj Bojańczyk, Bartek Klin, Joshua Moerman. Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata, 16 Seiten, 2021. https://arxiv.org/abs/2104.02438
DOI fulltext PDF [bibtex]
@article{R2021,
title = {Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {5},
pages = {pages 39},
type = {Journal Article},
year = {2021},
doi = {10.1145/3434320},
url = { https://publications.rwth-aachen.de/record/816245},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. 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.
DOI [bibtex]
@article{TM2021,
title = {The complexity of reachability in parametric Markov decision processes},
author = {Sebastian Junges and Joost-Pieter Katoen and Guillermo A. Pérez and Tobias Winkler},
publisher = {Elsevier},
journal = {Journal of computer and system sciences},
volume = {119},
pages = {pages 183-210},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jcss.2021.02.006},
url = { https://publications.rwth-aachen.de/record/816179},
}×
[issue] 		Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, Tobias Winkler. The complexity of reachability in parametric Markov decision processes, Journal of computer and system sciences 119, pages 183-210, Elsevier, 2021.
DOI fulltext PDF [bibtex]
@book{F2021,
title = {Foundations of probabilistic programming},
author = {},
editor = {Gilles Barthe and Joost-Pieter Katoen and Alexandra Silva},
publisher = {Cambridge University Press},
pages = {xiv, 568 Seiten : Illustrationen},
type = {Book},
year = {2021},
doi = {10.1017/9781108770750},
url = { https://publications.rwth-aachen.de/record/814578},
}×
[issue] 		Gilles Barthe (ed), Joost-Pieter Katoen (ed), Alexandra Silva (ed). Foundations of probabilistic programming, xiv, 568 Seiten : Illustrationen, Cambridge University Press, 2021.
DOI [bibtex]
@conference{GFPP2021,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
publisher = {Springer},
booktitle = {Theoretical Computer Science and General Issues},
volume = {12561},
pages = {231-248},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-68446-4_12},
url = { https://publications.rwth-aachen.de/record/807881},
}×
[issue] 		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
DOI fulltext PDF [bibtex]
@conference{BISMC2020,
title = {Bayesian Inference by Symbolic Model Checking},
author = {Bahare Salmani Barzoki and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12289},
pages = {115-133},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-59854-9_9},
url = { https://publications.rwth-aachen.de/record/814595},
}×
[issue] 		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.
DOI fulltext PDF [bibtex]
@article{I2020,
title = {Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control},
author = {Mingshuai Chen and Martin Fränzle and Yangjia Li and Peter N. Mosaad and Naijun Zhan},
publisher = {Springer},
journal = {Acta informatica},
volume = {58(5)},
pages = {pages 497-528},
type = {Journal Article},
year = {2020},
doi = {10.1007/s00236-020-00374-7},
url = { https://publications.rwth-aachen.de/record/783310},
}×
[issue] 		Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, Naijun Zhan. 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.
DOI fulltext PDF [bibtex]
@conference{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {512-538},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_27},
url = { https://publications.rwth-aachen.de/record/816242},
}×
[issue] 		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.
DOI [bibtex]
@conference{WPSBICCDD2020,
title = {Weakest Preexpectation Semantics for Bayesian Inference: Conditioning, Continuous Distributions and Divergence},
author = {Marcin Szymczak and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12154},
pages = {44-121},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-55089-9_3},
url = { https://publications.rwth-aachen.de/record/814579},
}×
[issue] 		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.
DOI arXiv:2007.06327 [bibtex]
@unpublished{GFPP2020,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
type = {Preprint},
year = {2020},
doi = {10.48550/ARXIV.2007.06327},
url = { https://arxiv.org/abs/2007.06327},
}×
[issue] 		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
DOI [bibtex]
@conference{RNA2020,
title = {Residual Nominal Automata},
author = {Joshua Moerman and Matteo Sammartino},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August},
booktitle = {Leibniz international proceedings in informatics},
volume = {171},
pages = {44:1-44:21},
type = {Conference Paper},
year = {2020},
doi = {10.4230/LIPIcs.CONCUR.2020.44},
url = { https://publications.rwth-aachen.de/record/804584},
}×
[issue] 		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.
DOI fulltext PDF [bibtex]
@conference{UTSVSDD2020,
title = {Unbounded-Time Safety Verification of Stochastic Differential Dynamics},
author = {Shenghua Feng and Mingshuai Chen and Bai Xue and Sriram Sankaranarayanan and Naijun Zhan},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {327-348},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_18},
url = { https://publications.rwth-aachen.de/record/794357},
}×
[issue] 		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.
DOI arXiv:2004.14835 [bibtex]
@unpublished{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schroer},
type = {Preprint},
year = {2020},
doi = {10.48550/ARXIV.2004.14835},
url = { https://arxiv.org/abs/2004.14835},
}×
[issue] 		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
DOI fulltext PDF [bibtex]
@conference{LOCTA2020,
title = {Learning One-Clock Timed Automata},
author = {Jie An and Mingshuai Chen and Bohua Zhan and Naijun Zhan and Miaomiao Zhang},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078, Theoretical Computer Science and General Issues},
pages = {444-462},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_25},
url = { https://publications.rwth-aachen.de/record/787949},
}×
[issue] 		Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. 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.
DOI fulltext PDF [bibtex]
@conference{SRNS2020,
title = {Separation and Renaming in Nominal Sets},
author = {Joshua Moerman and Jurriaan Rot},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, January},
booktitle = {Leibniz international proceedings in informatics},
volume = {152},
pages = {31:1-31:17},
type = {Conference Paper},
year = {2020},
doi = {10.4230/LIPIcs.CSL.2020.31},
url = { https://publications.rwth-aachen.de/record/786820},
}×
[issue] 		Joshua Moerman, Jurriaan Rot. 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
DOI [bibtex]
@conference{CDSPPS2019,
title = {Counterexample-Driven Synthesis for Probabilistic Program Sketches},
author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11800},
pages = {101-120},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-30942-8_8},
url = { https://publications.rwth-aachen.de/record/786831},
}×
[issue] 		Milan Češka, 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.
DOI arXiv:1906.00763 [bibtex]
@unpublished{SRNS2019,
title = {Separation and Renaming in Nominal Sets},
author = {Joshua Moerman and Jurriaan Rot},
pages = {23 Seiten},
type = {Preprint},
year = {2019},
doi = {10.48550/ARXIV.1906.00763},
url = { https://arxiv.org/abs/1906.00763},
}×
[issue] 		Joshua Moerman, Jurriaan Rot. Separation and Renaming in Nominal Sets, 23 Seiten, 2019. https://arxiv.org/abs/1906.00763
DOI arXiv:1910.11666 fulltext PDF [bibtex]
@unpublished{RNA2019,
title = {Residual Nominal Automata},
author = {Joshua Moerman and Matteo Sammartino},
pages = {25 Seiten},
type = {Preprint},
year = {2019},
doi = {10.48550/ARXIV.1910.11666},
url = { https://arxiv.org/abs/1910.11666},
}×
[issue] 		Joshua Moerman, Matteo Sammartino. Residual Nominal Automata, 25 Seiten, 2019. https://arxiv.org/abs/1910.11666
DOI [bibtex]
@inbook{MRR2019,
title = {Model Repair Revamped},
author = {Milan Češka and Hans Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11500},
pages = {107-125},
type = {Book Chapter},
year = {2019},
doi = {10.1007/978-3-030-31514-6_7},
url = { https://publications.rwth-aachen.de/record/768054},
}×
[issue] 		Milan Češka, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped, Volume 11500 of LNCS, 107-125, Springer, 2019.
DOI fulltext PDF [bibtex]
@conference{TQVBS2019,
title = {The Quantitative Verification Benchmark Set},
author = {Arnd Hartmanns and Michaela Klauck and David Parker and Tim Quatmann and Enno Ruijters},
publisher = {Springer},
booktitle = {LNCS},
volume = {11427},
pages = {344-350},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-17462-0_20},
url = { https://publications.rwth-aachen.de/record/759258},
}×
[issue] 		Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno Ruijters. The Quantitative Verification Benchmark Set, 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Volume 11427 of LNCS, 344-350, Springer, 2019.
DOI fulltext PDF [bibtex]
@phdthesis{A2019,
title = {Advanced weakest precondition calculi for probabilistic programs},
author = {Benjamin Lucien Kaminski},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (xiv, 363 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2019},
doi = {10.18154/RWTH-2019-01829},
url = { https://publications.rwth-aachen.de/record/755408},
}×
[issue] 		Benjamin Lucien Kaminski. Advanced weakest precondition calculi for probabilistic programs, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xiv, 363 Seiten) : Illustrationen, Diagramme, 2019.
DOI fulltext PDF [bibtex]
@article{Q2019,
title = {Quantitative separation logic: a logic for reasoning about probabilistic pointer programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {3(POPL)},
pages = {pages 34},
type = {Journal Article},
year = {2019},
doi = {10.1145/3290347},
url = { https://publications.rwth-aachen.de/record/753722},
}×
[issue] 		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
fulltext PDF [bibtex]
@article{DTLPSADDPVC2018,
title = {Digital Transformation of Lean Production: Systematic Approach for the Determination of Digitally Pervasive Value Chains},
author = {Peter Burggräf and Matthias Dannapfel and Hanno Arnd Voet and Patrick-Benjamin Bök and Jerome Uelpenich and Julian Hoppe},
publisher = {Apprimus Verlag},
journal = {International journal of industrial and manufacturing engineering},
volume = {17(10)},
pages = {pages 671-680},
type = {Journal Article},
year = {2018},
url = { https://publications.rwth-aachen.de/record/717232},
}×
[issue] 		Peter Burggräf, Matthias Dannapfel, Hanno Arnd Voet, Patrick-Benjamin Bök, Jerome Uelpenich, Julian Hoppe. Digital Transformation of Lean Production: Systematic Approach for the Determination of Digitally Pervasive Value Chains, International journal of industrial and manufacturing engineering 17 (10), pages 671-680, Apprimus Verlag, 2018.