Current Projects

CoCoS (website under construction)

The DFG funded project Constraint-Based Behavioral Consistency of Evolving Software Systems (CoCoS) is concerned with the following observation: The normative, anticipated behavior of a software system as envisaged during its development and the de facto, observed behavior emerging after its continued operation tend to drift apart, resulting in behavioral inconsistency. In CoCoS we investigate how behavioral consistency in software systems can be captured in technical and formal terms and we will implement a tool chain that can ensure it.

Control-Flow Fingerprinting for Malware Detection

This ATHENE funded project aims to detect malware based on a new, semantic approach called Control-Flow Fingerprinting. The idea is to compute a profile of a program's behavior by recording and classifying its logic decisions. The ambition is to be able to detect supply chain attacks targeting source code repositories.

KeY – A deductive Software Analysis Tool for the research community

This DFG Project aims to modernize and restructure the KeY verification system such that the wider research community can more easier adapt, contribute and benefit from KeY for their own research.

Model Centric Deductive Verification of Smart Contracts

This project is funded by ATHENE We are investigating how to ensure that smart contracts behave as intended.

The KeY Project

We have developed the KeY tool, which is a commercial tool for object-oriented software development augmented with a prover. The KeY tool allows users to develop guaranteed correct Java Card programs.

Past Projects


In ALBIA we develop a fully automatic logic-based information flow analysis. The analysis is based on an on-demand abstraction framework for a program logic calculus. This project has been part of the DFG Priority Program RS3.


The LOEWE project CompuGene is funded by the German State of Hesse. The goal is to develop computer-aided processes to enable the design of complex genetic circuits in biological systems, with a highly interdisciplinary approach. In our work we investigate how to enable formal modeling techniques developed in the computer science to be used for modeling and predicting biological systems.


Envisage is a research project on engineering virtualized services.


The project is funded as a project of the AG Signalling/DB RailLab between TU Darmstadt and Deutsche Bahn AG. It aims to provide a uniform model of operational and technical rulebooks for railroad operations. The model will allow automatic analysis with formal methods for properties like deadlock-freedom and throughput, but also be simulatable


The project is funded as a project of the AG Signalling/DB RailLab between TU Darmstadt and Deutsche Bahn AG. FormETCS aims to provide a uniform model for specifying ETCS equipped railway tracks. The model will allow to automate the planing and construction process of ETCS tracks.


Highly Adaptable and Trustworthy Software using Formal Methods, an Integrated Project supported by the 7th Framework Programme of the EC within the FET. In HATS we developed a methodological and tool framework to achieve not merely far-reaching automation in maintaining dynamically evolving software, but an unprecedented level of trust while informal processes are replaced with rigorous analyses based on formal semantics.


COST Action IC0901 is a European scientific cooperation. The main objective is making automated reasoning techniques and tools applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system users and developers.


COST Action IC0701 is a European scientific cooperation. The Action aims to develop verification technology with the reach and power to assure dependability of object-oriented programs on industrial scale.

Software Factory 4.0

The LOEWE project Software-Factory 4.0 (SF4.0) is a 4-year project funded by the German State of Hesse. SF4.0 is concerned with the adaptation of legacy software due to changed requirements and technical advances. We contribute to the project as leaders of part project B and as member of part project C.