59 citations · 458 across the 94 of their papers we have counts for
11 papers · 1 filter
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…
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
Qiuye Wang, Mingshuai Chen, Bai Xue +2
A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid s…
Parameter Synthesis in Markov Models: A Gentle Survey
Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
This paper surveys the analysis of parametric Markov models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations…
Towards Concurrent Quantitative Separation Logic
Ira Fesefeldt, Joost-Pieter Katoen, Thomas Noll
In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointe…
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg +1
We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the best of our knowledge, the first decidability…
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…
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen +2
Fault trees are a key model in reliability analysis. Classical static fault trees (SFT) can best be analysed using binary decision diagrams (BDD). State-based techniques are favora…
Inductive Synthesis of Finite-State Controllers for POMDPs
Roman Andriushchenko, Milan Ceska, Sebastian Junges +1
We present a novel learning framework to obtain finite-state controllers (FSCs) for partially observable Markov decision processes and illustrate its applicability for indefinite-h…
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…
Under-Approximating Expected Total Rewards in POMDPs
Alexander Bork, Joost-Pieter Katoen, Tim Quatmann
We consider the problem: is the optimal expected total reward to reach a goal state in a partially observable Markov decision process (POMDP) below a given threshold? We tackle thi…