66 citations · 568 across the 83 of their papers we have counts for
13 papers · 1 filter
Synthesizing Dominant Strategies for Liveness (Full Version)
Bernd Finkbeiner, Noemi Passing
Reactive synthesis automatically derives a strategy that satisfies a given specification. However, requiring a strategy to meet the specification in every situation is, in many cas…
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…
Explaining Hyperproperty Violations
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner +5
Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces…
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…
Formal Specifications from Natural Language
Christopher Hahn, Frederik Schmitt, Julia J. Tillman +3
We study the generalization abilities of language models when translating natural language into formal specifications with complex semantics. In particular, we fine-tune language m…
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Swen Jacobs, Guillermo A. Perez, Remco Abraham +22
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Th…
Attention Flows for General Transformers
Niklas Metzger, Christopher Hahn, Julian Siber +2
In this paper, we study the computation of how much an input token in a Transformer model influences its prediction. We formalize a method to construct a flow network out of the at…
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…
Real-time Visualization of Stream-based Monitoring Data
Jan Baumeister, Bernd Finkbeiner, Stefan Gumhold +1
Stream-based runtime monitors are used in safety-critical applications such as Unmanned Aerial Systems (UAS) to compute comprehensive statistics and logical assessments of system h…
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…
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…