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.
Petri Games: A Semantic and Algorithmic Approach for the Efficient Synthesis of Distributed Reactive Systems Petri Games
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.
Foundations of Perspicuous Software Systems CPEC
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.
Methods and Tools for Understanding and Controlling Privacy privacySFB
privacySFB provided conceptual and tangible contributions in several directions. This included 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.
Automatic Synthesis of Distributed and Parameterized Systems ASDPS
ASDPS aimed 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 studied approaches for the verification of distributed and parameterized systems and generalized the underlying ideas to develop novel methods for the more difficult task of automatic synthesis. This included 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.
Tradeoffs in Controller Synthesis TriCS
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?
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.