Formale Methoden für Systemkorrektheit / Formal Methods for the Correctness of Systems

Ein qualitativ hochwertiges Produkt der Informatik muss seine Aufgaben nicht nur schnell, ressourcensparend, optisch ansprechend und leicht bedienbar erfüllen, es muss nicht nur kostensparend herstellbar und wartbar sein, es muss auch funktionieren. In vielen Bereichen verbietet sich die "Reifung" des Produkts beim Anwender,weil ggf. Menschenleben oder auch nur Imageschaden des Herstellers bzw. hohe finanzielle Verluste die Folge sein können. Wir sind an der Entwicklung formal fundierter Technologien zur Sicherung funktionaler Korrektheit verschiedenster Systeme interessiert. Wir verfolgen sowohl das Paradigma "Korrektheit per Verifikation" als auch das der "Korrektheit per Konstruktion". Diesen beiden Paradigmen entsprechen ungefähr die beiden Forschungsrichtungen der Gruppe:

• Computergestützte Verifikation
• Algorithmen für Services

Usere Arbeiten zielen auf die Bereitstellung von leistungsstarken und frei zugänglichen Werkzeugen. Die Ergebnisse der Forschung werden in Lehrveranstaltungen auf Master-Level an die Studierenden weitergegeben.

High quality of a product related to computer science is not restricted to speed, ressource efficiency, graphical appearance, or usability. There is more about it than efficient production and maintenance. First and foremost, it should do its job correctly. In many areas, correctness cannot be achieved by letting the product "mature" at the customer since lives, or just the image or financial health of the prducer may depend on it. We are interested in the development of formally founded techniques for the assertion of correctness for various shapes of systems. We pursue both the paradigm of "correctness by verification" and the one of "correctness by construction". These two paradigms roughly correspond to our research areas

• Computer Aided Verification
• Algorithms for Services

We aim at turning our findings into powerful and freely available tools. Our results are passed to the students in lectures on master level.

Verbindung Theorie - Praxis / Closing the Gap Between Theory and Practice

In unserer Forschung zielen wir darauf ab, theoretisch fundierte Techniken in praktisch relevanten Szenarien gewinnbringend einzusetzen. Wir plädieren für eine generelle Abkehr von Agrenzungen zwischen Theorie und Praxis in der Informatik. Wir verwenden unsere Forschungsergebnisse, um Studienanfängern die Nützlichkeit der im Grundstudium gelehrten theoretischen Grundlagen der Informatik zu illustieren.

In our research efforts, we aim at the application of theoretically founded techniques to practically relevant problems. We generally reject traditional categorizations into "theory" and "practice" in computer science. We use our results for illustrating the usefulness of teaching theoretical foundations of computer science to undergraduate students.