43 citations · 96 across the 13 of their papers we have counts for
18 papers
Scaling Observation-aware Planning in Uncertain Domains
Adrian Zvizdenco, Arthur Conrado Veiga Bosquetti, Alberto Lluch Lafuente +1
Deciding which sensing capabilities to deploy on an agent in uncertain domains is a fundamental engineering challenge, in which one balances task achievability against the high cos…
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…
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…
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…
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…
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…
Flexible Refinement Proofs in Separation Logic
Aurea Bílá, Christoph Matheja, Peter Müller
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementatio…
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…
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…
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…
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen +2
We present quantitative separation logic (). In contrast to classical separation logic, employs quantities which evaluate to real numbers instead of pr…
Graph-Based Shape Analysis Beyond Context-Freeness
Hannah Arndt, Christina Jansen, Christoph Matheja +1
We develop a shape analysis for reasoning about relational properties of data structures. Both the concrete and the abstract domain are represented by hypergraphs. The analysis is…
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
Christina Jansen, Jens Katelaan, Christoph Matheja +2
We introduce heap automata, a formalism for automatic reasoning about robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates…
Inferring Covariances for Probabilistic Programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
We study weakest precondition reasoning about the (co)variance of outcomes and the variance of run-times of probabilistic programs with conditioning. For outcomes, we show that app…
Reasoning about Recursive Probabilistic Programs
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
This paper presents a wp-style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one-- an…
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja +1
This paper presents a wp-style calculus for obtaining bounds on the expected run-time of probabilistic programs. Its application includes determining the (possibly infinite) expect…