59 citations · 458 across the 94 of their papers we have counts for
123 papers
Towards a Deductive Verification Infrastructure for Weighted Programming
Emma Ahrens, Samuel Rode, Philipp Schröer +1
Weighted programs extend guarded commands with trace weights drawn from a semiring, or more generally a monoid-module. Varying this algebra gives one programmatic syntax for a vari…
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…
Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis
Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen
Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest…
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…
Adversarial Robustness of Time-Series Classification for Crystal Collimator Alignment
Xaver Fink, Borja Fernandez Adiego, Daniele Mirarchi +4
In this paper, we analyze and improve the adversarial robustness of a convolutional neural network (CNN) that assists crystal-collimator alignment at CERN's Large Hadron Collider (…
Compositional Reasoning for Probabilistic Automata with Uncertainty
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
This paper develops an assume-guarantee (AG) framework for the compositional verification of probabilistic automata (PAs) with uncertain transition probabilities. We study parametr…
Probabilistic Model Checking Taken by Storm
Matthias Volk, Linus Heck, Sebastian Junges +2
This tutorial paper presents a hands-on perspective on probabilistic model checking with the Storm model checker. Storm is a decade-old model checker that excels in performance and…
Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
Philipp Schröer, Joost-Pieter Katoen
We present a one-fits-all programmatic approach to reason about a plethora of objectives on probabilistic programs. The first ingredient is to add a reward-statement to the languag…
Verification of Robust Multi-Agent Systems
Raphaël Berthon, Joost-Pieter Katoen, Munyque Mittelmann +1
Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyber-physical infrastructures. In many such systems, howev…
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…
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…
Markov Decision Processes with Sure Parity and Multiple Reachability Objectives
Raphaël Berthon, Joost-Pieter Katoen, Tobias Winkler
This paper considers the problem of finding strategies that satisfy a mixture of sure and threshold objectives in Markov decision processes. We focus on a single -regular object…
A Spectrum of Approximate Probabilistic Bisimulations
Timm Spork, Christel Baier, Joost-Pieter Katoen +2
This paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation,…
Unknown Biases and Timing Constraints in Timed Automata
Darion Haase, Joost-Pieter Katoen
Timed automata are the formal model for real-time systems. Extensions with discrete probabilistic branching have been considered in the literature and successfully applied. Probabi…