Kevin Batz

Alumni

Member until: Dec 2024
Now at: Universität Münster, Germany
Address: Room 4203
Ahornstraße 55
D-52074 Aachen

I have joined the University of Münster as a Juniorprofessor of Computer Science. You can find my website here.

Publications

Own publications

2026

Conference paper
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
Programming languages and systems
PDF of Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops RWTH record for Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops BibTeX for Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Conference paper
Caesar: A Deductive Verifier for Probabilistic Programs
Philipp Schroer, Kevin Batz, Umut Yigit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Computer Aided Verification
PDF of Caesar: A Deductive Verifier for Probabilistic Programs RWTH record for Caesar: A Deductive Verifier for Probabilistic Programs BibTeX for Caesar: A Deductive Verifier for Probabilistic Programs
Conference paper
Verifying Sampling Algorithms via Distributional Invariants
Daniel Zilken, Kevin Batz, Joost-Pieter Katoen, Tobias Winkler
Formal Methods
PDF of Verifying Sampling Algorithms via Distributional Invariants RWTH record for Verifying Sampling Algorithms via Distributional Invariants BibTeX for Verifying Sampling Algorithms via Distributional Invariants

2025

Conference paper
Quantifier Elimination and Craig Interpolation: The Quantitative Way
Kevin Batz, Joost-Pieter Katoen, Nora Orhan
Foundations of Software Science and Computation Structures
PDF of Quantifier Elimination and Craig Interpolation: The Quantitative Way RWTH record for Quantifier Elimination and Craig Interpolation: The Quantitative Way BibTeX for Quantifier Elimination and Craig Interpolation: The Quantitative Way
Journal article
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
PDF of Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back RWTH record for Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back BibTeX for Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Book chapter
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, Part 1
RWTH record for 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 BibTeX for 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

2024

PhD thesis
Automated deductive verification of probabilistic programs
Kevin Batz
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Ichiro Hasuo
PDF of Automated deductive verification of probabilistic programs RWTH record for Automated deductive verification of probabilistic programs BibTeX for Automated deductive verification of probabilistic programs
Journal article
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
PDF of Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs RWTH record for Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs BibTeX for Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs

2023

Preprint
A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
PDF of A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)RWTH record for A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)BibTeX for A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
Journal article
A Deductive Verification Infrastructure for Probabilistic Programs
Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Proceedings of the ACM on programming languages
PDF of A Deductive Verification Infrastructure for Probabilistic Programs RWTH record for A Deductive Verification Infrastructure for Probabilistic Programs BibTeX for A Deductive Verification Infrastructure for Probabilistic Programs
Conference paper
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants RWTH record for Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants BibTeX for Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Journal article
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
PDF of A Calculus for Amortized Expected Runtimes RWTH record for A Calculus for Amortized Expected Runtimes BibTeX for A Calculus for Amortized Expected Runtimes

2022

Journal article
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
PDF of Weighted programming : a programming paradigm for specifying mathematical models RWTH record for Weighted programming : a programming paradigm for specifying mathematical models BibTeX for Weighted programming : a programming paradigm for specifying mathematical models
Conference paper
Foundations for Entailment Checking in Quantitative Separation Logic
Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll
Programming Languages and Systems
PDF of Foundations for Entailment Checking in Quantitative Separation Logic RWTH record for Foundations for Entailment Checking in Quantitative Separation Logic BibTeX for Foundations for Entailment Checking in Quantitative Separation Logic

2021

Conference paper
Latticed $k$-Induction with an Application to Probabilistic Programs
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
Computer-Aided Verification
PDF of Latticed $k$-Induction with an Application to Probabilistic Programs RWTH record for Latticed $k$-Induction with an Application to Probabilistic Programs BibTeX for Latticed $k$-Induction with an Application to Probabilistic Programs
Journal article
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
PDF of Relatively complete verification of probabilistic programs : an expressive language for expectation-based reasoning RWTH record for Relatively complete verification of probabilistic programs : an expressive language for expectation-based reasoning BibTeX for Relatively complete verification of probabilistic programs : an expressive language for expectation-based reasoning
Conference paper
Generating Functions for Probabilistic Programs
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler
Logic-Based Program Synthesis and Transformation
RWTH record for Generating Functions for Probabilistic Programs BibTeX for Generating Functions for Probabilistic Programs

2020

2019

Journal article
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
PDF of Quantitative separation logic: a logic for reasoning about probabilistic pointer programs RWTH record for Quantitative separation logic: a logic for reasoning about probabilistic pointer programs BibTeX for Quantitative separation logic: a logic for reasoning about probabilistic pointer programs

2018

Supervised theses

2024

Master’s thesis
A deductive verifier for probabilistic programs
Philipp Schroer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Peter Müller
Consultants: Kevin Batz, Benjamin Kaminski, Christoph Matheja
PDF of A deductive verifier for probabilistic programs RWTH record for A deductive verifier for probabilistic programs BibTeX for A deductive verifier for probabilistic programs
Master’s thesis
Distributional invariants for probabilistic programs
Daniel Johannes Zilken
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Kevin Batz, Tobias Winkler
RWTH record for Distributional invariants for probabilistic programs BibTeX for Distributional invariants for probabilistic programs
Bachelor’s thesis
Most probable explanations in Bayesian Networks via weighted programming
Dinis Vitorino
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler, Kevin Batz
PDF of Most probable explanations in Bayesian Networks via weighted programming RWTH record for Most probable explanations in Bayesian Networks via weighted programming BibTeX for Most probable explanations in Bayesian Networks via weighted programming

2022

Bachelor’s thesis
Automatic verification of loop invariants in weighted programs
Ben Sturgis
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler, Kevin Batz
RWTH record for Automatic verification of loop invariants in weighted programs BibTeX for Automatic verification of loop invariants in weighted programs

2021

Master’s thesis
Decidability and complexity of entailment checking in quantitative separation logic
Marvin Jansen
RWTH Aachen University
Advisers: Kevin Batz, Ira Justus Fesefeldt, Christoph Matheja, Joost-Pieter Katoen, Thomas Noll
RWTH record for Decidability and complexity of entailment checking in quantitative separation logic BibTeX for Decidability and complexity of entailment checking in quantitative separation logic

2020

Bachelor’s thesis
RPrIC3: PrIC3 for expected rewards
Adrian Gallus
RWTH Aachen University
Advisers: Kevin Batz, Joost-Pieter Katoen, Thomas Noll
RWTH record for RPrIC3: PrIC3 for expected rewards BibTeX for RPrIC3: PrIC3 for expected rewards

All records on RWTH Publications