39 citations · 99 across the 21 of their papers we have counts for
5 papers · 1 filter
Prophecy Variables for Hyperproperty Verification
Raven Beutner, Bernd Finkbeiner
Temporal logics for hyperproperties like HyperLTL use trace quantifiers to express properties that relate multiple system runs. In practice, the verification of such specifications…
Software Verification of Hyperproperties Beyond k-Safety
Raven Beutner, Bernd Finkbeiner
Temporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorith…
Deciding Hyperproperties Combined with Functional Specifications
Raven Beutner, David Carral, Bernd Finkbeiner +2
We study satisfiability for HyperLTL with a quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate mu…
Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming
Raven Beutner, Luke Ong, Fabian Zaiser
We propose a new method to approximate the posterior distribution of probabilistic programs by means of computing guaranteed bounds. The starting point of our work is an interval-b…
HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
Raven Beutner, Bernd Finkbeiner
Hyperproperties are system properties that relate multiple computation paths in a system and are commonly used to, e.g., define information-flow policies. In this paper, we study a…