Send email Copy Email Address
Research Group

Finkbeiner

Reactive Systems

Welcome! We develop methods for the design of systems that are provably safe and secure. Rooted in formal methods and mathematics, our techniques cover the entire software development process from requirements to deployment. We design expressive specification languages (temporal logics, hyperproperties), algorithms for automatic program synthesis and repair (controller synthesis, output-sensitive synthesis), and tools for static verification (MCHyper) and runtime monitoring and enforcement (RTLola). Our research has immediate impact in areas such as distributed, mobile, and autonomous systems and builds foundations that help us understand the digital systems defining tomorrow’s society.

Head of Group

Bernd Finkbeiner

Email

Address

Campus E1 1
66123 Saarbrücken (Germany)

Most Recent Publications

Year 2021

Conference / Medium

NFM
LNCS13th NASA Formal Methods Symposium, NFM 2021

Conference / Medium

TACAS
International Conference on Tools and Algorithms for the Construction and Analysis of SystemsTACAS: Tools and Algorithms for the Construction and Analysis of Systems

Year 2020

Conference / Medium

ATVA
Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020

Conference / Medium

ATVA
Lecture Notes in Computer ScienceAutomated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings

Conference / Medium

ATVA
LNCS, Volume 1230218th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020

TOOLS

New online interfaces: Try ADAM, BoSy, EAHyper, and MCHyper directly in your browser.

  • MCHyper is a model checker for hyperproperties.
  • Arctor is a termination prover for multi-threaded programs.
  • RESY is a requirement synthesis tool for compositional model checking.
  • dvt is a deductive verification tool for concurrent reactive systems. It supports verification of LTL properties, proving refinement relations, and translation validation.
  • SLAB is a certifying model checker for infinite state concurrent systems.

  • RVHyper is a runtime verification tool for temporal hyperproperties.
  • StreamLAB stream-based runtime monitoring.
  • MoCS synthesizes monitor circuits from linear time temporal logic formulas.
  • CirView is a small tool for 3D visualization of LTL path checking via boolean circuits.
  • DBA Minimizer is a tool calling an external SAT solver successively to minimize deterministic Büchi automata.
  • NBW Minimizer is a modified SAT-solver that performs minimization of non-deterministic Büchi automata.

  • BoSy is a reactive synthesis tool based on contraint solving.
  • SyFCo is a tool for reading, manipulating and transforming synthesis specifications in TLSF.
  • SafetySynth is synthesis tool based on solving safety games.
  • Synthia is a verification tool for checking safety requirements of open real-time systems modeled as networks of timed automata.
  • Unbeast synthesizes finite-state systems from LTL specifications using a symbolic implementation of the bounded synthesis approach.
  • Bassist synthesizes finite-state systems from ACTL ∩ LTL specifications.

  • EAHyper is a satisfiability solver for hyperproperties.
  • CAQE is a solver for quantified Boolean formulas in conjunctive normal form.
  • QuAbS is a solver for quantified Boolean formulas in negation normal form.
  • bunsat is a DQBF solver based on the bounded unsatisfiability method.
  • Caissa is a decision procedure for the quantifier-free theories of equality with uninterpreted symbols, integer linear arithmetic, fixed-size bit-vectors, arrays, sets, multisets, and lists with a length function.

CASE STUDIES

  • Syntroids is a game that is synthesized for FPGAs from TSL specifications.

PROJECTS

CURRENT PROJECTS

The goal of the OSARES project is the automatic synthesis of distributed embedded systems  that is, the construction of computer programs for such systems by a computer without the help of a human programmer.

The project is funded by the European Research Council for five years, from 2016 to 2021, as an ERC Consolidator Grant.

Further Information

This project develops a new setting for the synthesis of distributed systems where the synthesis problem can be solved with affordable cost, and that is, at the same time, sufficiently powerful to express the synthesis problems of realistic distributed systems. Our setting is based on Petri games, a game-theoretic extension of Petri nets. We extend Petri games to a full framework for the synthesis of distributed systems. The work targets both the semantic foundations of Petri games and efficient algorithms for solving Petri games. Overall, this project develops the first practical synthesis approach for distributed systems, including the necessary models, algorithms, and tools.

Further Information

This project aims at developing new methods and tools for the verification and synthesis of distributed and parameterized systems, such as communication protocols with a given or even a parametric number of components. To this end, we study approaches for the verification of distributed and parameterized systems and generalize the underlying ideas to develop novel methods for the more difficult task of automatic synthesis. This includes the development of efficient methods for the distributed synthesis problem with finite-state components, reductions from parameterized to distributed verification and synthesis, and methods for the synthesis of distributed infinite-state systems.

Further Information

From autonomous vehicles to Industry 4.0, from smart homes to smart cities – increasingly computer programs participate in actions and decisions that affect humans. However, our understanding of how these applications interact and what is the cause of a specific automated decision is lagging far behind. With the increase in cyber-physical technology impacting our lives, the consequences of this gradual loss in understanding are becoming severe. Systems lack support for making their behaviour plausible to their users. And even for technology experts it is nowadays virtually impossible to provide scientifically well-founded answers to questions about the exact reasons that lead to a particular decision, or about the responsibility for a malfunctioning. The root cause of the problem is that contemporary systems do not have any built-in concepts to explicate their behaviour. They calculate and propagate outcomes of computations, but are not designed to provide explanations. They are not perspicuous. The key to enable comprehension in a cyber-physical world is a science of perspicuous computing.

Further Information

This project will provide conceptual and tangible contributions in several directions. This includes for example models for identifying and quantifying private information, new techniques for hypothetically simulating user actions to assess their privacy impacts beforehand, and new algorithms for privacy-enhancing technologies for online interactions and mobile encounters. Achieving an overarching foundation for providing privacy in tomorrow’s Internet goes far beyond traditional security and privacy research. In our view it necessitates a paradigm shift to cope with the wealth and heterogeneity of user-to-user and user-to-provider interactions as well as the resulting challenges to privacy, requiring expertise from a wide range of computer science areas.

Further Information

COMPLETED PROJECTS

The goal of TriCS has been to increase the applicability of automated controller synthesis and to improve the quality of synthesized controllers by developing techniques to analyze tradeoffs between optimization criteria like size and quality of the controller, and by developing algorithms to compute controllers that are optimal with respect to more than one of these criteria. According to the state of the art there are two diverging approaches to synthesis: compute controllers within the upper bounds on memory requirements, but disregarding semantic quality, or to compute optimal controllers, which are much larger than the upper bounds. This raises the question whether there is a tradeoff between size and quality: are optimal controllers necessarily larger than generic ones?

AVACS raised the state of the art in automatic verification and analysis techniques from its current level, where it is applicable only to isolated facets (concurrency, time, continuous control, stability, dependability, mobility, data structures, hardware constraints, modularity, levels of refinement), to a level allowing the comprehensive verification of computer systems.

SpAGAT concerns the analysis of workflow systems where multiple users share a common document base. Secrecy and integrity are major issues in workflow systems when they handle sensitive data and common techniques like access control are often insufficient to prevent indirect flows of information. Information flow properties, that is specifications that abstractly characterize the legal flows of information, cover direct and indirect access to information alike. In SpAGAT we considered specification languages for information flow properties and we developed verification techniques to automatically prove information flow properties for workflow systems.

SpAGAT was funded by the DFG priority programme Reliably Secure Software Systems (RS3).

The BMBF-funded project Verisoft (“Beweisen als Ingenieurwissenschaft”) was a joint research project of TU Darmstadt, Universität Karlsruhe, Universität Koblenz, TU München, DFKI Saarbrücken, the Max-Planck Institut für Informatik, the Universität des Saarlandes, and several industrial partners including AbsInt, the BMW Group, Infineon Technologies, and T-Systems.

The goal of the project was the seamless verification of industrial computer systems through all layers, including the microprocessor, the operating system, and application programs. Work in the Verisoft project consisted of both practical verification tasks (formalizing and verifying benchmark systems from academia and industry) and tool development that supports the verification effort with automated techniques.