Author name cluster

Kevin Batz

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

2 author rows

FM Conference 2026 Conference Paper

Verifying Sampling Algorithms via Distributional Invariants

Daniel Zilken
Kevin Batz
Joost-Pieter Katoen
Tobias Winkler

Abstract This paper presents a Hoare-like verification framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso’s Fast Dice Roller and Saad et al. ’s Fast Loaded Dice Roller. These algorithms have previously resisted formal verification due to their probabilistic nature, intricate loop structure, and parametric input. Our approach complements existing proof rules based on inductive distributional invariants, enabling us to verify both total and partial correctness of the two algorithms.

DOI

LOPSTR Conference 2020 Conference Paper

Generating Functions for Probabilistic Programs

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

Abstract This paper investigates the usage of generating functions (GFs) encoding measures over the program variables for reasoning about discrete probabilistic programs. To that end, we define a denotational GF-transformer semantics for probabilistic while-programs, and show that it instantiates Kozen’s seminal distribution transformer semantics. We then study the effective usage of GFs for program analysis. We show that finitely expressible GFs enable checking super-invariants by means of computer algebra tools, and that they can be used to determine termination probabilities. The paper concludes by characterizing a class of—possibly infinite-state—programs whose semantics is a rational GF encoding a discrete phase-type distribution.

Details