Kevin Batz

According to our database, Kevin Batz authored at least 33 papers between 2018 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

Caesar: A Deductive Verifier for Probabilistic Programs.

Philipp Schröer, Kevin Batz, Umut Yigit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

CoRR, May, 2026

SMT-Based Active Learning of Weighted Automata.

Tiago Ferreira, Kevin Batz, Alexandra Silva

CoRR, May, 2026

Weighted NetKAT: A Programming Language For Quantitative Network Verification.

Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, Alexandra Silva

CoRR, April, 2026

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version).

Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler

CoRR, January, 2026

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops: Artifact.

Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler

Dataset, January, 2026

The Algebra of Iterative Constructions.

Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat, Todd Schmid

Arch. Formal Proofs, 2026

Verifying Sampling Algorithms via Distributional Invariants.

Daniel Zilken, Kevin Batz, Joost-Pieter Katoen, Tobias Winkler

Proceedings of the Formal Methods - 27th International Symposium, 2026

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

Proceedings of the Programming Languages and Systems, 2026

2025

Artifact for Paper Foundations for Deductive Verification of Continuous Probabilistic Programs.

Kevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler

Dataset, June, 2025

Artifact for Paper Foundations for Deductive Verification of Continuous Probabilistic Programs.

Kevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler

Dataset, April, 2025

Quantifier Elimination and Craig Interpolation: The Quantitative Way (Technical Report).

Kevin Batz, Joost-Pieter Katoen, Nora Orhan

CoRR, January, 2025

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back.

Kevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler

Proc. ACM Program. Lang., 2025

Quantifier Elimination and Craig Interpolation: The Quantitative Way.

Kevin Batz, Joost-Pieter Katoen, Nora Orhan

Proceedings of the Foundations of Software Science and Computation Structures, 2025

2024

Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs.

Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler

Proc. ACM Program. Lang., January, 2024

Automated deductive verification of probabilistic programs.

Kevin Batz

PhD thesis, 2024

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 (Technical Report).

Kevin Batz, Benjamin Lucien Kaminski, Christoph Matheja, Tobias Winkler

CoRR, 2024

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

Proceedings of the Principles of Verification: Cycling the Probabilistic Landscape, 2024

2023

A Deductive Verification Infrastructure for Probabilistic Programs.

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Proc. ACM Program. Lang., October, 2023

A Deductive Verification Infrastructure for Probabilistic Programs - Artifact Evaluation.

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Dataset, July, 2023

A Calculus for Amortized Expected Runtimes.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht

Proc. ACM Program. Lang., January, 2023

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.

Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

2022

Weighted programming: a programming paradigm for specifying mathematical models.

Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler

Proc. ACM Program. Lang., 2022

Weighted Programming.

Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler

CoRR, 2022

Foundations for Entailment Checking in Quantitative Separation Logic (extended version).

Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll

CoRR, 2022

Foundations for Entailment Checking in Quantitative Separation Logic.

Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll

Proceedings of the Programming Languages and Systems, 2022

2021

Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Proc. ACM Program. Lang., 2021

Latticed k-Induction with an Application to Probabilistic Programs.

Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Relatively Complete Verification of Probabilistic Programs.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

CoRR, 2020

Generating Functions for Probabilistic Programs.

Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler

Proceedings of the Logic-Based Program Synthesis and Transformation, 2020

PrIC3: Property Directed Reachability for MDPs.

Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll

Proc. ACM Program. Lang., 2019

2018

Quantitative Separation Logic.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll

CoRR, 2018

How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times.

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Proceedings of the Programming Languages and Systems, 2018