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 have been involved in the following teaching activities:

• 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 have supervised our student research assistants Philipp Schröer and Adrian Gallus as well as 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 (with Tobias Winkler)
• Nora Orhan, TBA, Bachelor’s Thesis, 2023
• Daniel Zilken, TBA, Master’s Thesis, ongoing work
• Dinis Vitorino, Bachelor’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

Conferences

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

Publications

2023
[bibtex] @article{ACAER2023, title = {A Calculus for Amortized Expected Runtimes}, author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Lena Verscht}, publisher = {ACM}, journal = {Proceedings of the ACM on programming languages}, volume = {7(POPL)}, pages = {pages 67}, type = {Journal Article}, year = {2023}, doi = {10.1145/3571260}, url = { https://publications.rwth-aachen.de/record/889639}, }× [issue]	Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht. A Calculus for Amortized Expected Runtimes, Proceedings of the ACM on programming languages 7 (POPL), pages 67, ACM, 2023.
[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.
[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.
[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
2022
[bibtex] @conference{FECQSL2022, title = {Foundations for Entailment Checking in Quantitative Separation Logic}, author = {Kevin Batz and Ira Justus Fesefeldt and Marvin Jansen and Joost-Pieter Katoen and Florian Keßler and Christoph Matheja and Thomas Noll}, publisher = {Springer}, booktitle = {LNCS}, volume = {13240}, pages = {57-84}, type = {Conference Paper}, year = {2022}, doi = {10.1007/978-3-030-99336-8_3}, url = { https://publications.rwth-aachen.de/record/843799}, }× [issue]	Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll. Foundations for Entailment Checking in Quantitative Separation Logic, 31. European Symposium on Programming (ESOP 2022), Volume 13240 of LNCS, 57-84, Springer, 2022.
[bibtex] @article{W2022, title = {Weighted programming: a programming paradigm for specifying mathematical models}, author = {Kevin Batz and Adrian Gallus and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Tobias Winkler}, publisher = {ACM}, journal = {Proceedings of the ACM on programming languages}, pages = {pages 66}, type = {Journal Article}, year = {2022}, doi = {10.1145/3527310}, url = { https://publications.rwth-aachen.de/record/845157}, }× [issue]	Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models, Proceedings of the ACM on programming languages, pages 66, ACM, 2022.
Show all