Komplexe Hard- und Softwaresysteme werden zunehmend auch in Anwendungen eingesetzt, die hohe Anforderungen an Sicherheit und Verfügbarkeit stellen. Prominente Beispiele sind Flugzeug- und Bremssteuerungen, aber auch Anwendungen im Finanzbereich. Hier stößt klassisches Testen an seine Grenzen. Daher werden formale, d.h. mathematik-basierte Methoden in diesen Gebieten jetzt auch in der industriellen Praxis zunehmend genutzt: Während Airbus schon lange auf formale Methoden setzt, hat Boeing erst kürzlich den Einsatz formaler Methoden für obligatorisch erklärt. Auch Microsoft verwendet inzwischen Softwareverifikationstechniken, um die Zuverlässigkeit von Device-Treibern zu erhöhen. Die Theorie der Programmierung beschäftigt sich mit den Grundlagen derartiger formaler Methoden. Sie beantwortet dabei u.a. die folgenden Fragen: - Was ist die Bedeutung eines Programmes und wie kann man sie mathematisch erfassen? (Semantik) - Wie kann man beweisen, dass ein Programm das tut, was es soll? (Verifikation) - Welche Techniken gibt es, um Eigenschaften von Programmen automatisch, d.h. rechnergestützt auszurechnen oder zu überprüfen? (Automatische Analyse und Model Checking) Programmierung und Softwareentwurf sind zentrale Themen für den Informatiker. Das durch die Beschäftigung mit der Theorie der Programmierung erworbene vertiefte Verständnis dieser Themen und insbesondere der Korrektheitsproblematik hilft, gute und fehlerfreie Software zu konstruieren, auch dann, wenn dies ohne Einsatz formaler Methoden geschieht. Deshalb sollte sich jeder Informatiker in seinem Studium mit der Theorie der Programmierung beschäftigt haben.
- Lehrende/r: Sebastian Kenter
- Lehrende/r: Markus Müller-Olm