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.
Abgeschlossene Projekte
ALBIA
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
Envisage is a research project on engineering virtualized services.
FormbaR
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
FormETCS
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.
HATS
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 IC0901
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 IC0701
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.