- 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
| 2024 | |
|---|---|
[bibtex]
[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 | |
|
[bibtex]
[issue]
|
Kevin Batz, , Joost-Pieter Katoen, , Lena Verscht. A Calculus for Amortized Expected Runtimes, Proceedings of the ACM on programming languages 7 (POPL), pages 67, ACM, 2023. |
|
[bibtex]
[issue]
|
Kevin Batz, Mingshuai Chen, Sebastian Junges, , Joost-Pieter Katoen, . 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. |
|
[bibtex]
[issue]
|
Philipp Schroer, Kevin Batz, , Joost-Pieter Katoen, . A Deductive Verification Infrastructure for Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA2), pages 294, ACM, 2023. |
|
[bibtex]
[issue]
|
Philipp Schroer, Kevin Batz, , Joost-Pieter Katoen, . A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version), [1]-48, 2023. https://arxiv.org/abs/2309.07781 |
| Show all | |