66 citations · 568 across the 83 of their papers we have counts for
75 papers · 1 filter
Logics and Algorithms for Hyperproperties
Bernd Finkbeiner
System requirements related to concepts like information flow, knowledge, and robustness cannot be judged in terms of individual system executions, but rather require an analysis o…
Counterfactuals Modulo Temporal Logics
Bernd Finkbeiner, Julian Siber
Lewis' theory of counterfactuals is the foundation of many contemporary notions of causality. In this paper, we extend this theory in the temporal direction to enable symbolic coun…
Second-Order Hyperproperties
Raven Beutner, Bernd Finkbeiner, Hadar Frenkel +1
We introduce HyperLTL, a temporal logic for the specification of hyperproperties that allows for second-order quantification over sets of traces. Unlike first-order temporal lo…
Automata-Based Software Model Checking of Hyperproperties
Bernd Finkbeiner, Hadar Frenkel, Jana Hofmann +1
We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal Logic (LTL) with memory…
AutoHyper: Explicit-State Model Checking for HyperLTL
Raven Beutner, Bernd Finkbeiner
HyperLTL is a temporal logic that can express hyperproperties, i.e., properties that relate multiple execution traces of a system. Such properties are becoming increasingly importa…
Bounded Model Checking for Asynchronous Hyperproperties
Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner +1
Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in (e.g., schedulers and asynchronous communication…