Laufende Projekte

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.

FormETCS (website under construction)

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.

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.

Abgeschlossene Projekte


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.


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 simulatableEnvisage


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.