185.323 Verifikation von Übersetzern
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2011S, VU, 2.0h, 3.0EC, wird geblockt abgehalten

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

Ziele:

  • Kenntnis der Methoden der Übersetzerverifikation.
  • An Hand einfacher Beispiele selbstständig Übersetzer verifizieren können.

Aufbau der Vorlesung:

  1. Einleitung (Was heißt Korrektheit von Übersetzern?)
  2. Grundlagen und Semantik von Programmiersprachen
  3. Korrektheit der Speicherabbildung
  4. Korrektheit der Zwischencodeeerzeugung
  5. Korrektheit der Codeerzeugung und der Assemblierung

Inhalt der Lehrveranstaltung

Die Vorlesung setzt Grundkenntnisse des Übersetzerbaus, etwa aus der Vorlesung Übersetzerbau, voraus. Empfehlenswert ist auch der vorige Besuch der Vorlesung "Weiterführender Übersetzerbau". Bei sicherheitskritischen Anwendungen dürfen oft nur einfachste Übersetzer verwendet werden bzw. müssen direkt in Maschinensprache programmiert werden. Ursache hierfür ist mangelndes Vertrauen in die korrekte Funktionsweise von Übersetzern. In der Tat gibt es bei ausgelieferten Übersetzern so viele Fehler, dass durch die Verwendung handelsüblicher oder öffentlicher Übersetzer oft nicht die notwendige Zuverlässigkeit sicherheitskritischer Anwendungen erreicht werden kann. Das Thema dieser Vorlesung behandelten Methoden sollten zukünftig den Einsatz optimierender Übersetzer auch im sicherheitskritischen Bereich ermöglichen. Die Methoden und Vorgehensweisen orientieren sich an den im Projekt Verifix erarbeiteten Resultate. In der Vorlesung wird an Hand einer einfachen Programmiersprache die Konstruktion eines korrekten Übersetzers demonstriert. Korrektheit heißt im weiteren Sinne, dass der vom Übersetzer erzeugte Code die Semantik des zu übersetzenden Programms erhält. Dazu ist es zunächst notwendig, aufzuzeigen, wie man eine formale Semantik einer Programmiersprache definieren kann (wir verwenden hier abstrakte Zustandsmaschinen). Anschließend wird für jede der einzelnen Übersetzerschritte gezeigt, wie man deren Korrektheit nachweist. Man unterscheidet die Verifikation der Transformationsregeln (Erhaltung der Semantik) und deren Implementierung im Übersetzer. Für Ersteres verwendet man eine Technik ähnlich den Simulationsbeweisen aus der Komplexitäts- und Berechenbarkeitstheorie, für Letzteres wird für jeden Übersetzeraufruf überprüft, ob die Transformationsregeln korrekt angewendet wurden. Nur mit beidem zusammen kann man die Korrektheit von Übersetzern sicherstellen.

Weitere Informationen

Die Vorlesung wird im Rahmen einer ERASMUS/LLP-Vereinbarung zwischen der TU Wien und der Martin-Luther-Universität Halle-Wittenberg, Deutschland, von Professor Dr. habil. Wolf Zimmermann als Blockveranstaltung in der Zeit vom 01.03.2011 bis zum 11.03.2011 gehalten. Die Vorbesprechung zur Lehrveranstaltung findet zum ersten Veranstaltungstermin am 01.03.2011 um 16:00 Uhr statt. Der Veranstaltungsort ist die Bibliothek des Arbeitsbereichs für Programmiersprachen und Übersetzer in der Argentinierstr. 8, 4. Stock (Mitte), 1040 Wien.

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Do.09:00 - 12:0003.03.2011Seminarraum Argentinierstrasse 185.323 Verifikation von Übersetzern
Di.09:00 - 12:0008.03.2011Seminarraum FAV EG B (Seminarraum von Neumann) 185.323: Verifikation von Übersetzern
Do.09:00 - 12:0010.03.2011FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) 185.323 Verifikation von Übersetzern
LVA wird geblockt abgehalten

LVA-Anmeldung

Nicht erforderlich

Curricula

Literatur

Wird in der Vorlesung bekannt gegeben.

Vorkenntnisse

Vorkenntnisse aus dem Übersetzerbau etwa in dem in den LVAs 185.311 (und 185.274) vermittelten Umfang sind wünschenswert.

Vorausgehende Lehrveranstaltungen

Begleitende Lehrveranstaltungen

Weitere Informationen

Sprache

Deutsch