Publications

The Algebra of Iterative Constructions Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat, Todd Schmid. LICS 2026, to appear.
Caesar: A Deductive Verifier for Probabilistic Programs Philipp Schröer, Kevin Batz, Umut Yiğit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. CAV 2026, to appear.
Weighted NetKAT: A Programming Language for Quantitative Network Verification Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, Alexandra Silva. PLDI 2026, to appear.
SMT-Based Active Learning of Weighted Automata Tiago Ferreira, Kevin Batz, Alexandra Silva. CAV 2026, to appear.
Verifying Sampling Algorithms via Distributional Invariants Daniel Zilken, Kevin Batz, Joost-Pieter Katoen, Tobias Winkler. Formal Methods (FM), 2026, pp. 259-278. doi
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. ESOP 2026, pp. 314-343. doi

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back Kevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler. Proceedings of the ACM on Programming Languages 9 (OOPSLA1), 2025, pp. 421-448. doi
Quantifier Elimination and Craig Interpolation: The Quantitative Way Kevin Batz, Joost-Pieter Katoen, Nora Orhan. FoSSaCS 2025, pp. 176-197. doi

Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Proceedings of the ACM on Programming Languages 8 (POPL), 2024, pp. 2792-2820. doi
J-P: MDP. FP. PP. Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler. Principles of Verification: Cycling the Probabilistic Landscape, Springer, 2024, pp. 255-302. doi
Latticed Craig Interpolation with an Application to Probabilistic Verification Mingqi Yang, Kevin Batz, Mingshuai Chen, Joost-Pieter Katoen, Zhiang Wu, Jianwei Yin. Workshop on Theory and Applications of Craig Interpolation and Beth Definability (CIBD), 2024. Extended abstract.

A Deductive Verification Infrastructure for Probabilistic Programs Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 2023, pp. 2052-2082. doi
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. TACAS 2023, pp. 410-429. doi
A Calculus for Amortized Expected Runtimes Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht. Proceedings of the ACM on Programming Languages 7 (POPL), 2023, pp. 1957-1986. doi

Weighted Programming: A Programming Paradigm for Specifying Mathematical Models Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler. Proceedings of the ACM on Programming Languages 6 (OOPSLA1), 2022, pp. 1-30. doi
Foundations for Entailment Checking in Quantitative Separation Logic Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll. ESOP 2022, pp. 57-84. doi

Latticed k-Induction with an Application to Probabilistic Programs Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. CAV 2021, pp. 524-549. doi
Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Proceedings of the ACM on Programming Languages 5 (POPL), 2021, pp. 1-30. doi
Generating Functions for Probabilistic Programs Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. LOPSTR 2020, pp. 231-248. doi

PrIC3: Property Directed Reachability for MDPs Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. CAV 2020, pp. 512-538. doi

Quantitative Separation Logic: A Logic for Reasoning About Probabilistic Pointer Programs Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Proceedings of the ACM on Programming Languages 3 (POPL), 2019, pp. 34:1-34:29. doi