Kevin Batz

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:

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 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, winner of the Berthold Vöcking Master Award (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

Publications

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 fulltext PDF [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.
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 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 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
2022
DOI fulltext PDF [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.
DOI fulltext PDF [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.
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.
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 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.
2020
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},
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
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},
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
arXiv:2010.14548 [bibtex]
@unpublished{RCVPP2020,
title = {Relatively Complete Verification of Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
pages = {49 Seiten},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2010.14548},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Relatively Complete Verification of Probabilistic Programs, 49 Seiten, 2020. https://arxiv.org/abs/2010.14548
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.
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
DOI fulltext PDF [bibtex]
@conference{HOBIA2018,
title = {How long, O Bayesian network, will I sample thee?: A program analysis perspective on expected sampling times},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {10801},
pages = {186-213},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89884-1_7},
url = { https://publications.rwth-aachen.de/record/753062},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. How long, O Bayesian network, will I sample thee?: A program analysis perspective on expected sampling times, 27. European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, 186-213, Springer, 2018.
arXiv:1802.10467 [bibtex]
@unpublished{QSLALRPP2018,
title = {Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
pages = {159 Seiten},
type = {Preprint},
year = {2018},
url = { https://arxiv.org/abs/1802.10467},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs, 159 Seiten, 2018. https://arxiv.org/abs/1802.10467