59 citations · 458 across the 94 of their papers we have counts for
10 papers · 1 filter
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
Philipp Schröer, Darion Haase, Joost-Pieter Katoen
This paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. Our key principle is based on providing slices for (1) error…
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…
Compositional Reasoning for Parametric Probabilistic Automata
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic…
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
Raphaël Berthon, Joost-Pieter Katoen, Zihan Zhou
Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from sto…
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Timm Spork, Christel Baier, Joost-Pieter Katoen +2
We introduce -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsilo…
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl +1
We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a se…
Bayesian Inference in Quantum Programs
Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen
Conditioning is a key feature in probabilistic programming to enable modeling the influence of data (also known as observations) to the probability distribution described by such p…
Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
Linus Heck, Tim Quatmann, Jip Spel +2
Parametric Markov chains (pMCs) are Markov chains (MCs) with symbolic probabilities. A pMC encodes a family of MCs, where each member is obtained by replacing parameters with const…
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…