Theorie der Programmierung (Sommersemester 2019)

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

Übungen: Prof. Dr. Markus Müller-Olm, Jens Gutsfeld, Sebastian Kenter

Eintrag für diese Veranstaltung im HIS/LSF

Learnweb-Kurs zu dieser Veranstaltung

Hinweise

Die erste Vorlesung ist am Montag, dem 01.04.2019.

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 ZIV-Benutzerkennung mit Passwort; der Einschreibeschlüssel zum Zugriff auf diesen Kurs wird in der ersten Vorlesung bekannt gegeben.

Ort und Zeit

Vorlesung: Mo 10:15-12:00 Uhr, M5 und Do 10:15-12:00 Uhr, M5

Übung: Mi 10:15-12:00 Uhr, M5

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:

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.

Literatur

Krzysztof R. Apt, Frank S. de Boer und Ernst-Rüdiger Olderog. Verification of Sequential and Concurrent Programs, Springer-Verlag, 3. Auflage, 2009.
Eike Best. Semantik: Theorie sequentieller und paralleler Programmierung, Vieweg, 1995.
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.
Nissim Francez. Program Verification, Addison-Wesley, 1992.
Jacques Loeckx und Kurt Sieber. The Foundations of Program Verification, Wiley-Teubner, 2. Auflage, 1987.
Hanne Riis Nielson und Flemming Nielson. Semantics with Applications: An Appetizer, Springer-Verlag, 2010.
Flemming Nielson, Hanne Riis Nielson und Chris Hankin. Principles of Program Analysis, Springer-Verlag, 1999.
Ernst-Rüdiger Olderog und Bernhard Steffen. Kapitel "Formale Semantik und Programmverifikation" in: Informatik-Handbuch, Hrsg.: Peter Rechenberg und Gustav Pomberger, Hanser, 2002.