66 citations · 110 across the 8 of their papers we have counts for
13 papers · 1 filter
Realizing Omega-regular Hyperproperties
Bernd Finkbeiner, Christopher Hahn, Jana Hofmann +1
We studied the hyperlogic HyperQPTL, which combines the concepts of trace relations and -regularity. We showed that HyperQPTL is very expressive, it can express properties like…
Efficient Monitoring of Hyperproperties using Prefix Trees
Bernd Finkbeiner, Christopher Hahn, Marvin Stenger +1
Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other and are thus not monitorable by tools that consider comp…
Verifying Hyperliveness
Norine Coenen, Bernd Finkbeiner, César Sánchez +1
HyperLTL is an extension of linear-time temporal logic for the specification of hyperproperties, i.e., temporal properties that relate multiple computation traces. HyperLTL can exp…
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
Bernd Finkbeiner, Christopher Hahn, Marvin Stenger +1
We present RVHyper, a runtime verification tool for hyperproperties. Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces wit…
Constraint-Based Monitoring of Hyperproperties
Christopher Hahn, Marvin Stenger, Leander Tentrup
Verifying hyperproperties at runtime is a challenging problem as hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with ea…
Synthesizing Reactive Systems from Hyperproperties
Bernd Finkbeiner, Christopher Hahn, Philip Lukert +2
We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to…