We develop algorithms and tools for the synthesis and verification of reactive systems.
Output-Sensitive Algorithms for Reactive Synthesis OSARES
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.
Tradeoffs in Controller Synthesis TriCS
The goal of this project is 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?
Automatic Synthesis of Distributed and Parameterized Systems ASDPS
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.
Automatic Verification And Analysis of Complex Systems AVACS
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.
Secrecy and Information Flow in Shared Document Bases SpAGAT
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.