Finkbeiner

• 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.

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

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.