38 citations · 61 across the 8 of their papers we have counts for
8 papers · 1 filter
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…
Smart Contract Synthesis Modulo Hyperproperties
Norine Coenen, Bernd Finkbeiner, Jana Hofmann +1
Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transaction…
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…
Reactive Synthesis of Smart Contract Control Flows
Bernd Finkbeiner, Jana Hofmann, Florian Kohn +1
Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic constructio…
Runtime Enforcement of Hyperproperties
Norine Coenen, Bernd Finkbeiner, Christopher Hahn +2
An enforcement mechanism monitors a reactive system for undesired behavior at runtime and corrects the system's output in case it violates the given specification. In this paper, w…
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…
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
Jonni Virtema, Jana Hofmann, Bernd Finkbeiner +2
We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining…
The Hierarchy of Hyperlogics
Norine Coenen, Bernd Finkbeiner, Christopher Hahn +1
Hyperproperties, which generalize trace properties by relating multiple traces, are widely studied in information-flow security. Recently, a number of logics for hyperproperties ha…