Research

Our research concerns computer-aided methods for the synthesis and verification of reactive systems.

Current Projects

Automatic Verification And Analysis of Complex Systems – AVACS

The goal of AVACS is to raise 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

The subject of this project is the analysis of secrecy and information flow in applications where multiple users execute a workflow while sharing a common document base. Our objective is to generalize classic notions of secrecy such as noninterference so that the designer can precisely state the intended information flow as it changes over time in response to changes in the state of the workflow as well as strategic choices by the different users of the system. The new specification language will be supported by a semantically substantiated security analysis based on a multi-player game model of the interaction between the users. Extending counterexample-guided abstraction refinement (CEGAR) to such models, we will obtain automatic methods for verification and certificate synthesis.

Completed Projects

Verisoft

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.