Email

kevin.batz at cs.rwth-aachen.de

Address

Room 4203
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21206

I am a PhD candidate and member of the FRAPPANT project at the Software Modeling and Verification Group headed by Professor J.-P. Katoen. My research interests include the semantics of (heap-manipulating) probabilistic programs as well as techniques and calculi enabling their (preferably automated) verification. Moreover, I have co-developed Weighted Programming — a programming paradigm for specifying mathematical models.

You can find me on dblp and Google Scholar.

Teaching

I gave a lecture on the automatic verification of probabilistic programs in Prof. Katoen’s course on probabilistic programming.

Moreover, I have been involved in the following teaching activities:

• Static Program Analysis (SS 24)
• Semantics and Verification of Software (SS 23)
• Compiler Construction (WS 22/23)
• Static Program Analysis (SS 22)
• Concurrency Theory (SS 21)
• Semantics and Verification of Software (SS 21)
• Compiler Construction (WS 20/21)
• Seminar: Probabilistic Programming
• Static Program Analysis (SS 20)
• Proseminar: Introduction to Program Analysis (SS 20)
• Concurrency Theory (WS 19/20)
• Semantics and Verification of Software (SS 19)

Supervision

I am supervising our student research assistant Nora Orhan. In the past, I have supervised our student research assistants Philipp Schröer and Adrian Gallus, our intern Zhiang Wu, and our postgraduate intern Tom Biskup.

Moreover, I am supervising or have supervised the following thesis projects:

• Florian Keßler, On the Decidability of Entailment Checking in Quantitative Separation Logics, Bachelor’s Thesis, 2020, winner of the CS Department Award 2020 (with Thomas Noll and Christoph Matheja).
• Adrian Gallus, RPrIC3: PrIC3 for Expected Rewards, Bachelor’s Thesis, 2020
• Marvin Jansen, Decidability and Complexity of Entailment Checking in Quantitative Separation Logic, Master’s Thesis, 2021, winner of the CS Department Award 2021 (with Ira Fesefeldt and Christoph Matheja)
• Philipp Schröer, A Deductive Verifier for Probabilistic Programs, Master’s Thesis, 2022 (with Benjamin Kaminski and Christoph Matheja)
• Ben Sturgis, Bachelor’s Thesis, Automatic Verification of Loop Invariants in Weighted Programs, 2022 (with Tobias Winkler)
• Tom Biskup, Invariant-based Strategy Synthesis for Nondeterministic Probabilistic Programs, Master’s Thesis, 2023, winner of the Berthold Vöcking Master Award (with Tobias Winkler)
• Nora Orhan, TBA, Bachelor’s Thesis, 2023
• Daniel Zilken, TBA, Master’s Thesis, 2024
• Dinis Vitorino, TBA, Bachelor’s Thesis, 2024
• Daniel Basgöze, TBA, Master’s Thesis, ongoing work

Awards

• Our paper A Deductive Verification Infrastructure for Probabilistic Programs (joint work with Philipp Schröer, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja) has received a distinguished artifact award at OOPSLA 2023.
• Our paper Generating Functions for Probabilistic Programs (joint work with Lutz Klinkenberg, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman and Tobias Winkler) has received the best paper award at LOPSTR 2020.
• I was awarded the Springorum Medal in 2019 for receiving a master’s degree with distinction.
• Our paper How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times (joint work with Benjamin Kaminski, Joost-Pieter Katoen, and Christoph Matheja) was nominated for the EATCS Best Paper Award at ETAPS 2018.

External Reviewer

• POPL 2025
• FMSD
• FMSD
• CAV 2024
• LICS 2024
• FoSSaCS 2024
• UAI 2023
• POPL 2023
• POPL 2022 (Artifact Evaluation)
• LICS 2022
• LICS 2021
• CAV 2021 (regular paper & artifact evaluation)
• TACAS 2021
• CONCUR20
• LPAR23
• QEST 2019

Publications

2025
[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.
2024
[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.
[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.
Show all