Theorie der Programmierung (Sommersemester 2021)

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

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

Eintrag für diese Veranstaltung im HIS/LSF
Learnweb-Kurs zu dieser Veranstaltung

Hinweise

  • Wegen der Coronapandemie wird diese Veranstaltung in einer alternativen Form angeboten. Wenn Sie teilnehmen möchten, tragen Sie sich bitte bis spätestens 12. April in den Learnweb-Kurs ein. Bis dahin wird eine Einschreibung ohne Einschreibeschlüssel möglich sein. Danach erfragen Sie bitte den Einschreibeschlüssel per E-Mail bei einem der Veranstalter.
  • Am Montag, dem 12. April 2021, um 10:15 Uhr findet eine Auftaktveranstaltung im Livestream per Zoom statt. Die Zugangsdaten finden Sie im Learnwebkurs.
  • Alle weiteren Informationen finden Sie im Learnweb-Kurs.

Ort und Zeit

  • Vorlesungen: Mo 10:15-11:45 Uhr und Do 10:15-11:45 Uhr
  • Übungen: Mi 10:15-12:00 Uhr

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 jetzt 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:

  1. Was ist die Bedeutung eines Programmes und wie kann man sie mathematisch präzise erfassen? (Semantik)
  2. Wie kann man beweisen, dass ein Programm tut, was es soll? (Verifikation)
  3. 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.