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