Vorlesung: Theorie der Programmierung
Veranstaltung im Sommersemster 2025 an der Universität Münster
Vorlesung: Prof. Dr. Markus Müller-Olm
Übungen: Prof. Dr. Markus Müller-Olm, Roman Lakenbrink
Eintrag für diese Veranstaltung im HIS/LSF
Ort und Zeit
Vorlesungen: Mo 10:15-11:45 Uhr und Do 10:15-11:45 Uhr, M6
Übungen: Mi 10:15-11:45 Uhr, M6
Vorlesungsinhalt
Komplexe Hard- und Softwaresysteme werden heutzutage auch in vielen 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 auch in der industriellen Praxis zunehmend genutzt: Airbus setzt schon sehr lange auf formale Methoden und auch bei Boeing ist der Einsatz formaler Methoden inzwischen obligatorisch. Auch Microsoft verwendet schon seit längerem 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)
Programmierung und Softwareentwicklung sind zentrale Themen für Informatikerinnen und Informatiker. Das durch die Beschäftigung mit der Theorie der Programmierung erworbene vertiefte Verständnis dieser Themen im Hinblick auf die Korrektheitsproblematik hilft, gute und fehlerfreie Software zu konstruieren, auch dann, wenn dies ohne Einsatz formaler Methoden geschieht.