Bernd Finkbeiner

research

∙ 06/15/2023

Counterfactuals Modulo Temporal Logics

Lewis' theory of counterfactuals is the foundation of many contemporary ...

0 Bernd Finkbeiner, et al. ∙

research

∙ 05/29/2023

Second-Order Hyperproperties

We introduce Hyper^2LTL, a temporal logic for the specification of hyper...

0 Raven Beutner, et al. ∙

research

∙ 03/26/2023

Automata-Based Software Model Checking of Hyperproperties

We develop model checking algorithms for Temporal Stream Logic (TSL) and...

0 Bernd Finkbeiner, et al. ∙

research

∙ 03/02/2023

Iterative Circuit Repair Against Formal Specifications

We present a deep learning approach for repairing sequential circuits ag...

0 Matthias Cosler, et al. ∙

research

∙ 01/26/2023

AutoHyper: Explicit-State Model Checking for HyperLTL

HyperLTL is a temporal logic that can express hyperproperties, i.e., pro...

0 Raven Beutner, et al. ∙

research

∙ 01/17/2023

Bounded Model Checking for Asynchronous Hyperproperties

Many types of attacks on confidentiality stem from the nondeterministic ...

0 Tzu-Han Hsu, et al. ∙

research

∙ 10/04/2022

Synthesizing Dominant Strategies for Liveness (Full Version)

Reactive synthesis automatically derives a strategy that satisfies a giv...

0 Bernd Finkbeiner, et al. ∙

research

∙ 08/15/2022

Smart Contract Synthesis Modulo Hyperproperties

Smart contracts are small but highly security-critical programs that imp...

0 Norine Coenen, et al. ∙

research

∙ 06/07/2022

Software Verification of Hyperproperties Beyond k-Safety

Temporal hyperproperties are system properties that relate multiple exec...

0 Raven Beutner, et al. ∙

research

∙ 06/04/2022

Explaining Hyperproperty Violations

Hyperproperties relate multiple computation traces to each other. Model ...

0 Norine Coenen, et al. ∙

research

∙ 06/04/2022

Formal Specifications from Natural Language

We study the generalization abilities of language models when translatin...

0 Christopher Hahn, et al. ∙

research

∙ 06/03/2022

Prophecy Variables for Hyperproperty Verification

Temporal logics for hyperproperties like HyperLTL use trace quantifiers ...

0 Raven Beutner, et al. ∙

research

∙ 06/01/2022

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021

We report on the last four editions of the reactive synthesis competitio...

0 Swen Jacobs, et al. ∙

research

∙ 05/30/2022

Attention Flows for General Transformers

In this paper, we study the computation of how much an input token in a ...

0 Niklas Metzger, et al. ∙

research

∙ 05/30/2022

Deciding Hyperproperties Combined with Functional Specifications

We study satisfiability for HyperLTL with a ∀^*∃^* quantifier prefix, kn...

0 Raven Beutner, et al. ∙

research

∙ 05/24/2022

Information Flow Guided Synthesis (Full Version)

Compositional synthesis relies on the discovery of assumptions, i.e., re...

0 Bernd Finkbeiner, et al. ∙

research

∙ 05/12/2022

Reactive Synthesis of Smart Contract Control Flows

Smart contracts are small but highly error-prone programs that implement...

0 Bernd Finkbeiner, et al. ∙

research

∙ 03/14/2022

A Logic for Hyperproperties in Multi-Agent Systems

Hyperproperties are commonly used in computer security to define informa...

0 Raven Beutner, et al. ∙

research

∙ 03/08/2022

Runtime Enforcement of Hyperproperties

An enforcement mechanism monitors a reactive system for undesired behavi...

0 Norine Coenen, et al. ∙

research

∙ 11/09/2021

RTLola on Board: Testing Real Driving Emissions on your Phone

This paper is about shipping runtime verification to the masses. It pres...

0 Sebastian Biewer, et al. ∙

research

∙ 08/08/2021

Visual Analysis of Hyperproperties for Understanding Model Checking Results

Model checkers provide algorithms for proving that a mathematical model ...

0 Tom Horak, et al. ∙

research

∙ 07/25/2021

Neural Circuit Synthesis from Specification Patterns

We train hierarchical Transformers on the task of synthesizing hardware ...

0 Frederik Schmitt, et al. ∙

research

∙ 07/25/2021

Model Checking Algorithms for Hyperproperties

Hyperproperties generalize trace properties by expressing relations betw...

0 Bernd Finkbeiner, et al. ∙

research

∙ 07/20/2021

Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory

In the synthesis of distributed systems, we automate the development of ...

0 Bernd Finkbeiner, et al. ∙

research

∙ 07/06/2021

A Temporal Logic for Strategic Hyperproperties

Hyperproperties are commonly used in computer security to define informa...

0 Raven Beutner, et al. ∙

research

∙ 07/02/2021

Live Synthesis

Synthesis automatically constructs an implementation that satisfies a gi...

0 Bernd Finkbeiner, et al. ∙

research

∙ 06/28/2021

Compositional Synthesis of Modular Systems (Full Version)

Given the advances in reactive synthesis, it is a natural next step to c...

0 Bernd Finkbeiner, et al. ∙

research

∙ 05/29/2021

Causality-Based Game Solving

We present a causality-based algorithm for solving two-player reachabili...

0 Christel Baier, et al. ∙

research

∙ 04/30/2021

Temporal Stream Logic modulo Theories

Temporal Stream Logic (TSL) is a temporal logic that extends LTL with up...

0 Bernd Finkbeiner, et al. ∙

research

∙ 04/28/2021

A Temporal Logic for Asynchronous Hyperproperties

Hyperproperties are properties of computational systems that require mor...

0 Jan Baumeister, et al. ∙

research

∙ 03/15/2021

Specification Decomposition for Reactive Synthesis (Full Version)

Reactive synthesis is the task of automatically deriving an implementati...

0 Bernd Finkbeiner, et al. ∙

research

∙ 01/19/2021

Controller Synthesis for Hyperproperties

We investigate the problem of controller synthesis for hyperproperties s...

0 Borzoo Bonakdarpour, et al. ∙

research

∙ 01/19/2021

Program Repair for Hyperproperties

We study the repair problem for hyperproperties specified in the tempora...

0 Borzoo Bonakdarpour, et al. ∙

research

∙ 01/19/2021

The Complexity of Monitoring Hyperproperties

We study the runtime verification of hyperproperties, expressed in the t...

0 Borzoo Bonakdarpour, et al. ∙

research

∙ 01/18/2021

Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications

We present Syntroids, a case study for the automatic synthesis of hardwa...

0 Gideon Geier, et al. ∙

research

∙ 01/18/2021

Realizing Omega-regular Hyperproperties

We studied the hyperlogic HyperQPTL, which combines the concepts of trac...

0 Bernd Finkbeiner, et al. ∙

research

∙ 01/18/2021

Efficient Monitoring of Hyperproperties using Prefix Trees

Hyperproperties, such as non-interference and observational determinism,...

0 Bernd Finkbeiner, et al. ∙

research

∙ 12/29/2020

Synthesizing Approximate Implementations for Unrealizable Specifications

The unrealizability of a specification is often due to the assumption th...

0 Rayna Dimitrova, et al. ∙

research

∙ 12/29/2020

Approximate Automata for Omega-Regular Languages

Automata over infinite words, also known as omega-automata, play a key r...

0 Rayna Dimitrova, et al. ∙

research

∙ 12/29/2020

Canonical Representations of k-Safety Hyperproperties

Hyperproperties elevate the traditional view of trace properties form se...

0 Bernd Finkbeiner, et al. ∙

research

∙ 12/29/2020

Explainable Reactive Synthesis

Reactive synthesis transforms a specification of a reactive system, give...

0 Tom Baumeister, et al. ∙

research

∙ 12/15/2020

Verified Rust Monitors for Lola Specifications

The safety of cyber-physical systems rests on the correctness of their m...

0 Bernd Finkbeiner, et al. ∙

research

∙ 10/07/2020

Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

We study the expressivity and the model checking problem of linear tempo...

0 Jonni Virtema, et al. ∙

research

∙ 07/14/2020

Model Checking Branching Properties on Petri Nets with Transits (Full Version)

To model check concurrent systems, it is convenient to distinguish betwe...

0 Bernd Finkbeiner, et al. ∙

research

∙ 07/14/2020

Dependency-based Compositional Synthesis (Full Version)

Despite many recent advances, reactive synthesis is still not really a p...

0 Bernd Finkbeiner, et al. ∙

research

∙ 05/15/2020

Verifying Hyperliveness

HyperLTL is an extension of linear-time temporal logic for the specifica...

0 Norine Coenen, et al. ∙

research

∙ 05/14/2020

AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)

The correctness of networks is often described in terms of the individua...

0 Bernd Finkbeiner, et al. ∙

research

∙ 05/12/2020

The Hierarchy of Hyperlogics

Hyperproperties, which generalize trace properties by relating multiple ...

0 Norine Coenen, et al. ∙

research

∙ 05/07/2020

Probabilistic Hyperproperties of Markov Decision Processes

We study the specification and verification of hyperproperties for proba...

0 Rayna Dimitrova, et al. ∙

research

∙ 03/27/2020

RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft

The autonomous control of unmanned aircraft is a highly safety-critical ...

0 Jan Baumeister, et al. ∙

Bernd Finkbeiner

Featured Co-authors