Ankündigung Vortrag

Im Rahmen des Kolloquiums des Instituts für Informatik hält

Herr Dr. David Sabel (KIST, Uni Frankfurt)
am Dienstag, den 13.11.2012 um 14 c.t.
in Seminarraum 11 (Robert-Mayer-Str. 11-15, EG)

einen Vortrag zum Thema
"Korrektheit von Programmen und Programmiersprachen"

Zusammenfassung:

Die Korrektheit von Programmen ist zweifellos ein Kernthema der Informatik von enormer praktischer Relevanz. Es gibt hierzu viele weit entwickelte Ansätze und Methoden wie denotationale Semantiken, Hoare Logiken und Erweiterungen (z.B. Separation Logic),  die jedoch meist nur sehr stark eingeschränkte Modelle von Programmiersprachen behandeln können, und/oder deren mathematische Werkzeuge nur von wenigen Experten durchschaut werden.


Im Vortrag wird der Ansatz der kontextuellen Semantik vorgestellt, der auf rein informatischen Methoden und Vorgehensweisen aufbaut, ein sehr breites Spektrum  von Programmsprachen und Fragstellungen abdeckt, und im Wesentlichen mit den zwei einfachen folgenden Konzepten auskommt:

  • Die formale Beschreibung der Auswertung von Programmen (als operationale Semantik), und

  • die Beobachtung des Verhaltens.

Diese Vorgehensweise ist flexibel genug, um moderne Programmiersprachen zu behandeln, die Konstrukte höherer Ordnung, nebenläufige, parallele und nichtdeterministische Auswertungen erlauben.

Innerhalb des Vortrags werden Varianten von Programmiersprachen ebenso wie verschiedene Anwendungsbereiche der Korrektheit beleuchtet, die mit leichten Variationen der Basisbegriffe zu weitreichenden Ergebnissen führen.

Beispielsweise benötigt man einen Korrektheitsbegriff für Programmtransformationen, die innerhalb innerhalb ein und derselben Programmiersprache durchgeführt werden. Dieser ist jedoch abzugrenzen vom Begriff der Korrektheit von Übersetzungen einer höheren Programmiersprache in eine aschinennähere Sprache. Ebenso erfordern nichtdeterministische und nebenläufige Programmiersprachen andere Korrektheitsbegriffe als rein sequentielle Programmiersprachen.

Im Vortrag werden Forschungsergebnisse in diesem Umfeld vorgestellt, die belegen, dass man aufbauend auf den einfachen Konzepten verlässliche Aussagen zur Korrektheit von Programmtransformationen, zu Übersetzungen und Implementierungen als auch zu Logiken über Programme, für konkrete, moderne Programmiersprachen erhält.

Zusätzliche Informationen