43 citations · 69 across the 16 of their papers we have counts for
24 papers
Type-Directed Discretization of Probabilistic Programs (Extended Version)
Katherine Wu, Jules Jacobs, Kevin Batz +1
We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where co…
Multiobjective Preexpectation Reasoning for Probabilistic Programs
Lena Verscht, Hannah Mertens, Kevin Batz +3
Probabilistic programs with nondeterminism model planning problems in which a strategy typically resolves the nondeterminism to meet a specification. We study the multiobjective se…
A Fast Quantitative Analyzer for NetKAT
Thomas Lu, Qiancheng Fu, Kevin Batz +5
When designing a network, engineers must navigate trade-offs (e.g., one topology offers more aggregate bandwidth, another lower latency or better resilience) that demand reasoning…
Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams
Daniel Basgöze, Kevin Batz, Sebastian Junges +1
Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive verification approaches aim to establish bounds on these q…
Caesar: A Deductive Verifier for Probabilistic Programs
Philipp Schröer, Kevin Batz, Umut Yiğit Dural +4
Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL all…
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…
SMT-Based Active Learning of Weighted Automata
Tiago Ferreira, Kevin Batz, Alexandra Silva
We present an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/L*-style methods. Our algorithm is p…
Weighted NetKAT: A Programming Language For Quantitative Network Verification
Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz +3
We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatmen…
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)
Darion Haase, Kevin Batz, Adrian Gallus +4
A fundamental computational task in probabilistic programming is to infer a program's output (posterior) distribution from a given initial (prior) distribution. This problem is cha…
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…
A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski +2
This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie…
A Calculus for Amortized Expected Runtimes
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen +2
We develop a weakest-precondition-style calculus à la Dijkstra for reasoning about amortized expected runtimes of randomized algorithms with access to dynamic memory - the $\textsf…
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Kevin Batz, Mingshuai Chen, Sebastian Junges +3
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet eff…
Weighted Programming
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski +2
We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs…
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
Kevin Batz, Ira Fesefeldt, Marvin Jansen +4
Quantitative separation logic (QSL) is an extension of separation logic (SL) for the verification of probabilistic pointer programs. In QSL, formulae evaluate to real numbers inste…
Relatively Complete Verification of Probabilistic Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
We study a syntax for specifying quantitative "assertions" - functions mapping program states to numbers - for probabilistic program verification. We prove that our syntax is expre…
Generating Functions for Probabilistic Programs
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski +3
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 de…
PrIC3: Property Directed Reachability for MDPs
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski +3
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our…
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 +1
Bayesian networks (BNs) are probabilistic graphical models for describing complex joint probability distributions. The main problem for BNs is inference: Determine the probability…
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen +2
We present quantitative separation logic (). In contrast to classical separation logic, employs quantities which evaluate to real numbers instead of pr…