E-mail senden E-Mail Adresse kopieren
Forschungsgruppe

Finkbeiner

Reaktive Systeme

Wir entwickeln Methoden für den Entwurf von Systemen, die nachweislich sicher sind. Unsere Techniken sind in formalen Methoden und Mathematik verwurzelt und decken den gesamten Softwareentwicklungsprozess ab, von den Anforderungen bis zum Einsatz. Wir entwerfen ausdrucksstarke Spezifikationssprachen (temporale Logiken, Hyperproperties), Algorithmen für die automatische Programmsynthese und -reparatur (Controller-Synthese, ausgangssensitive Synthese) sowie Werkzeuge für die statische Verifikation (MCHyper) und die Laufzeitüberwachung und -durchsetzung (RTLola). Unsere Forschung hat unmittelbare Auswirkungen auf Bereiche wie verteilte, mobile und autonome Systeme und schafft Grundlagen, die uns helfen, die digitalen Systeme zu verstehen, die die Gesellschaft von morgen bestimmen.

Gruppenleiter:in

Bernd Finkbeiner

E-Mail

Adresse

Campus E1 1
66123 Saarbrücken (Germany)

Neueste Veröffentlichungen

Jahr 2023

Konferenz / Medium

ATVA
ATVA 2023 - International Symposium on Automated Technology for Verification and AnalysisATVA 2023

Konferenz / Medium

CAV
Lecture Notes in Computer Science (LNCS, volume 13965)35th International Conference on Computer Aided Verification (CAV 2023)

Konferenz / Medium

CAV
Computer Aided VerificationCAV 2023

Konferenz / Medium

LPAR
Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and ReasoningLPAR-23

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.