43 citations · 96 across the 13 of their papers we have counts for
4 papers · 1 filter
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…