47 citations · 183 across the 23 of their papers we have counts for
34 papers
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…
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…
noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning
Tobias Gürtler, Benjamin Lucien Kaminski
Probabilistic programming languages (PPLs) are an expressive and intuitive means of representing complex probability distributions. In that realm, languages like Dice target an imp…
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…
Programming and Reasoning in Partially Observable Probabilistic Environments
Tobias Gürtler, Benjamin Lucien Kaminski
Probabilistic partial observability is a phenomenon occuring when computer systems are deployed in environments that behave probabilistically and whose exact state cannot be fully…
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…
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski +1
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing cal…
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…
The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions
Akihisa Yamada, Benjamin Lucien Kaminski, Dieter Hofbauer +2
This report contains the proceedings of the 19th International Workshop on Termination (WST 2023), which was held in Obergurgl during August 24--25 as part of Obergurgl Summer on R…
Lower Bounds for Possibly Divergent Probabilistic Programs
Shenghua Feng, Mingshuai Chen, Han Su +3
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the ca…
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…
Quantitative Strongest Post
Linpeng Zhang, Benjamin Lucien Kaminski
We present a novel strongest-postcondition-style calculus for quantitative reasoning about non-deterministic programs with loops. Whereas existing quantitative weakest pre allows r…
Probabilistic Data with Continuous Distributions
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
Statistical models of real world data typically involve continuous probability distributions such as normal, Laplace, or exponential distributions. Such distributions are supported…
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…
Generative Datalog with Continuous Distributions
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
Arguing for the need to combine declarative and probabilistic programming, Bárány et al. (TODS 2017) recently introduced a probabilistic extension of Datalog as a "purely declarati…
Optimistic Value Iteration
Arnd Hartmanns, Benjamin Lucien Kaminski
Markov decision processes are widely used for planning and verification in settings that combine controllable or adversarial choices with probabilistic behaviour. The standard anal…
Aiming Low Is Harder -- Induction for Lower Bounds in Probabilistic Program Verification
Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl +1
We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our…
A Pre-Expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu +3
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone func…
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…