Mathematische Logik und Anwendungen
| project description | contact
|
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.
The Graduiertenkolleg addresses a coherent subject matter ranging from fundamental algebraic questions to applications in the information technology. The studies program is constructed so that participating graduate students and postdoctoral fellows develop a broad expertise in these topics. More details can be found [here].
The group for Computer Architecture in this project deals with (Bounded) Model Checking for Hybrid Systems: Numerous embedded systems operate with or themselves consist of coupled networks of discrete and continuous components as well. The behaviour of such systems cannot be understood without an explicit modelling of the interaction between discrete and continuous components. While tools for synthesis and simulation exist, verification tools are just at their starting point.
On the other hand, Model Checking and Bounded Model Checking are well established in the digital hardware domain. A successful transfer of these approaches to the domain of "hybrid systems" is the main goal of this project. In particular, new ideas the proof methods are necessary.