66 citations · 568 across the 83 of their papers we have counts for
19 papers · 1 filter
RTLola on Board: Testing Real Driving Emissions on your Phone
Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns +3
This paper is about shipping runtime verification to the masses. It presents the crucial technology enabling everyday car owners to monitor the behaviour of their cars in-the-wild.…
Monitoring with Verified Guarantees
Dauer J. C., Finkbeiner B., Schirmer S
Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For e…
Visual Analysis of Hyperproperties for Understanding Model Checking Results
Tom Horak, Norine Coenen, Niklas Metzger +6
Model checkers provide algorithms for proving that a mathematical model of a system satisfies a given specification. In case of a violation, a counterexample that shows the erroneo…
Neural Circuit Synthesis from Specification Patterns
Frederik Schmitt, Christopher Hahn, Markus N. Rabe +1
We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications in linear-time temporal logic (LTL). The LTL synt…
Model Checking Algorithms for Hyperproperties
Bernd Finkbeiner
Hyperproperties generalize trace properties by expressing relations between multiple computations. Hyperpropertes include policies from information-flow security, like observationa…
A Temporal Logic for Strategic Hyperproperties
Raven Beutner, Bernd Finkbeiner
Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations.…
Live Synthesis
Bernd Finkbeiner, Felix Klein, Niklas Metzger
Synthesis automatically constructs an implementation that satisfies a given logical specification. In this paper, we study the live synthesis problem, where the synthesized impleme…
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specificatio…
Compositional Synthesis of Modular Systems (Full Version)
Bernd Finkbeiner, Noemi Passing
Given the advances in reactive synthesis, it is a natural next step to consider more complex multi-process systems. Distributed synthesis, however, is not yet scalable. Composition…
Causality-Based Game Solving
Christel Baier, Norine Coenen, Bernd Finkbeiner +3
We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of pro…
A Temporal Logic for Asynchronous Hyperproperties
Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour +2
Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a tra…
Temporal Stream Logic modulo Theories (Full Version)
Bernd Finkbeiner, Philippe Heim, Noemi Passing
Temporal stream logic (TSL) extends LTL with updates and predicates over arbitrary function terms. This allows for specifying data-intensive systems for which LTL is not expressive…
Specification Decomposition for Reactive Synthesis
Bernd Finkbeiner, Gideon Geier, Noemi Passing
Reactive synthesis is the task of automatically deriving a correct implementation from a specification. It is a promising technique for the development of verified programs and har…
Controller Synthesis for Hyperproperties
Borzoo Bonakdarpour, Bernd Finkbeiner
We investigate the problem of controller synthesis for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple executio…
Program Repair for Hyperproperties
Borzoo Bonakdarpour, Bernd Finkbeiner
We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple computation traces. This class…
The Complexity of Monitoring Hyperproperties
Borzoo Bonakdarpour, Bernd Finkbeiner
We study the runtime verification of hyperproperties, expressed in the temporal logic HyperLTL, as a means to inspect a system with respect to security polices. Runtime monitors fo…
Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
Gideon Geier, Philippe Heim, Felix Klein +1
We present Syntroids, a case study for the automatic synthesis of hardware from a temporal logic specification. Syntroids is a space shooter arcade game realized on an FPGA, where…
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…