Theorie der Programmierung (Sommersemester 2023)

Vorlesung: Prof. Dr. Markus Müller-Olm

Übungen: Prof. Dr. Markus Müller-Olm, Jens Gutsfeld, Roman Lakenbrink, Christoph Ohrem

Eintrag für diese Veranstaltung im HIS/LSF

 Learnwebkurs zu dieser Veranstaltung

Hinweise

  • Die erste Vorlesung ist am Montag, dem 3.4.2023, um 10:15 Uhr im Hörsaal M5
  • Aktuelle Informationen, Folien und Übungsblätter zu dieser Veranstaltung werden im zugehörigen Learnweb-Kurs veröffentlicht. Zum Login auf der Learnweb-Plattform genügt Ihre WWU-Benutzerkennung mit Passwort; der Einschreibeschlüssel zum Zugriff auf diesen Kurs wird in der ersten Vorlesung bekannt gegeben.

Ort und Zeit

Vorlesungen: Mo 10:15-11:45 Uhr und Do 10:15-11:45 Uhr, M5

Übungen: Fr 12:15-13:45 Uhr, M2

Vorlesungsinhalt

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 als ein Mittel, Fehlerfreiheit sicherzustellen, an seine Grenzen. Daher werden formale, d.h. mathematik-basierte Methoden in diesen Gebieten auch in der industriellen Praxis zunehmend genutzt: Während Airbus schon lange auf formale Methoden setzt, hat auch Boeing seit einiger Zeit den Einsatz formaler Methoden für obligatorisch erklärt. Auch Microsoft verwendet inzwischen Softwareverifikationstechniken, um die Zuverlässigkeit von Gerätetreibern 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 präzise erfassen? (Semantik)
  • Wie kann man beweisen, dass ein Programm tut, was es soll? (Verifikation)
  • Welche Techniken gibt es, um Eigenschaften von Programmen automatisch, d.h. rechnergestützt auszurechnen? (Automatische Analyse und Model Checking)

Programmierung und Softwareentwicklung 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.