22 citations · 26 across the 13 of their papers we have counts for
10 papers · 1 filter
The Algebra of Iterative Constructions
Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer +3
Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructi…
Verifying Sampling Algorithms via Distributional Invariants
Daniel Zilken, Kevin Batz, Joost-Pieter Katoen +1
This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saa…
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Kevin Batz, Joost-Pieter Katoen, Francesca Randone +1
We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) co…
Quantifier Elimination and Craig Interpolation, Quantitatively
Kevin Batz, Joost-Pieter Katoen, Nora Orhan
Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware and software verification. They are rooted in the…
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 +1
Markov decision processes (MDPs) with rewards are a widespread and well-studied model for systems that make both probabilistic and nondeterministic choices. A fundamental result ab…
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen +1
We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that…