27 citations · 38 across the 6 of their papers we have counts for
14 papers
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…
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…
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…