185.276 Analyse und Verifikation
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

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

Merkmale

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

Ziele der Lehrveranstaltung

Die Studierenden erhalten ein profundes theoretisches und praktisches
Verständnis fundamentaler Prinzipien und Konzepte in Programmanalyse,
-verifikation und -transformation, das sie befähigt, darauf gegründete
Verfahren kompetent und adäqat anzuwenden und die Möglichkeiten und
Grenzen insbesondere automatischer Verfahren zur Programmanalyse,
-verifikation und -transformation fundiert einzuschätzen und zu
beurteilen.

Inhalt der Lehrveranstaltung

Die Vorlesung beschäftigt sich mit Konzepten und Prinzipien
grundlegender und fortgeschrittener Verfahren zur Analyse und
Verifikation von Softwaresystemen. Im Mittelpunkt stehen dabei die
Konzepte von Korrektheit, Vollständigkeit und Optimalität in Analyse,
Verifikation und Transformation. Die Vorlesung spannt dabei den Bogen
von Hoarescher Logik über Programm- und Datenflussanalyse zur
Theorie abstrakter Interpretation und Modellprüfung. Illustrierende
Transformationen werden dabei besonders dem Bereich optimierender und
verifizierender Übersetzung entnommen. Anhand regelmäßig gestellter
Übungsaufgaben werden die in der Vorlesung behandelten Themen an
maßgeschneiderten Aufgabenstellungen erprobt und angewendet.

Teil I: Motivation

  • Grundlagen
  • Operationelle Semantik von WHILE
  • Denotationelle Semantik von WHILE
  • Axiomatische Semantik von WHILE
  • Worst-Case Execution Time Analyse

Teil II: Analyse und Verifikation

  • Programmanalyse
  • Programmverifikation vs. Programmanalyse
  • Reverse Datenflussanalyse
  • Chaotische Fixpunktiteration
  • Basisblock- vs. Einzelanweisungsgraphen

Teil III: Transformation und Optimalität

  • Elimination partiell toter Anweisungen
  • Elimination partiell redundanter Anweisungen
  • Kombination von PRAE und PDCE
  • Konstantenfaltung auf dem Wertegraphen

Teil IV: Abstrakte Interpretation und Modellprüfung

  • Abstrakte Interpretation und DFA
  • Modellprüfung und DFA

Teil V: Abschluss und Ausblick

  • Resümee und Perspektiven




Weitere Informationen

Vorauss. am Mittwoch, den 01.03.2017, findet von 13 Uhr s.t. bis 14 Uhr im
Hösaal EI4 eine gemeinsame Vorbesprechung für alle am AB
Programmiersprachen und Übersetzer im SS 2017 angebotenen
Lehrveranstaltungen statt.

Eine spezifische Vorbesprechung für die LVA "Analyse und Verifikation"
findet zusammen mit der ersten Vorlesung am Mi, den 01.03.2017, um
17:00 Uhr c.t. im Hörsaal EI3a, Elektrot.Institutsg., Gußhausstr. 25-29, 2. Stock, statt.

Aufteilung der ECTS-Punkte:

Der Lehrveranstaltung sind 3.0 ECTS-Punkte zugeordnet. Diese
entsprechen einem durchschnittlichen Lernaufwand von 75
Stunden. Dieser durchschnittliche Lernaufwand verteilt sich in
folgender Weise auf die einzelnen Teile der Lehrveranstaltung:

  • Vorlesungsbesuch und -vor- und -nachbereitung: 35 Std.
  • Übungsaufgaben: 30 Std.
  • Prüfungsvorbereitung und mündliche Prüfung: 10 Std.

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mi.16:00 - 18:0001.03.2017 - 28.06.2017EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Fr.14:00 - 16:0007.04.2017EI 3A Hörsaal LVA 185.276 Analyse und Verifikation
Mi.17:00 - 19:0007.06.2017EI 3A Hörsaal LVA 185.276 Analyse und Verifikation
Analyse und Verifikation - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.01.03.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.08.03.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.15.03.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.22.03.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.29.03.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.05.04.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Fr.07.04.201714:00 - 16:00EI 3A Hörsaal LVA 185.276 Analyse und Verifikation
Mi.26.04.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.03.05.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.10.05.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.17.05.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.24.05.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.31.05.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.07.06.201717:00 - 19:00EI 3A Hörsaal LVA 185.276 Analyse und Verifikation
Mi.14.06.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.21.06.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.28.06.201716:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
LVA wird geblockt abgehalten

Leistungsnachweis

Beurteilung von Beispielen und mündliche Prüfung. Die Gesamtnote setzt
sich je zur Hälfte aus der Übungsnote auf die Beispiele und der Note
für die mündliche Prüfung zusammen.

LVA-Anmeldung

Von Bis Abmeldung bis
01.03.2017 12:00 10.03.2017 12:00 31.03.2017 12:00

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Grundlegende Kenntnisse in Theoretischer Informatik und Programmierung
werden vorausgesetzt. Kenntnisse im Übersetzerbau sind nützlich, etwa
aus den Lehrveranstaltungen 185.A48 VU 4.0h "Übersetzerbau" oder
185.A04 VU 2.0 "Optimierende Compiler", aber nicht zwingend
erforderlich.

Die Vorlesung ergänzt die Lehrveranstaltungen 185.A04 "Optimierende
Compiler" und 185.A56 "Semantik von Programmiersprachen". Sie
empfiehlt sich deshalb inbesondere für Studierende, die im Bereich von
Programmiersprachen und Übersetzerbau einen besonderen Schwerpunkt
setzen, eine Seminararbeit, ein Praktikum oder ihre Diplomarbeit
anfertigen möchten.

Vorausgehende Lehrveranstaltungen

Begleitende Lehrveranstaltungen

Vertiefende Lehrveranstaltungen

Weitere Informationen

Sprache

Deutsch