Projects
AVACS
The project addresses the rigorous mathematical verification and analysis of models and realizations of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. Our aim is to raise the state of the art in automatic verification and analysis techniques (v&a) from a 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 a comprehensive and holistic verification of such systems.
Salomo
In this project, computer science and jurisprudence jointly develop a concept for the planning, design, and management of contracts between small and medium-sized enterprises (SMEs) regarding the development of software. The idea is to turn an easily composed, yet efficient and machine-readable specification of the requirements of the software to be developed and the automatic verification of the requirements into a constituent part of the development contract. The design of this contract ensures legal relevance of the technical verification results.
Verisoft XT
The main goal of the project is the pervasive formal verification of computer systems. The correct functionality of systems, as they are used, for example, in automotive engineering, in security technology and in the sector of medical technology, is to be mathematically proved.
Graduiertenkolleg
Over the past century, mathematical logic has developed from a foundationally oriented science to a mathematical discipline, enriching traditional areas of mathematics with new ideas, methods, and results. The numerous and diverse connections to computer science, whose origins lies in part in mathematical logic, have led to the mutual advancement of both disciplines. This Graduiertenkolleg focuses on the interplay between logic and computer science/mathematics.