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.

2020S, VU, 2.0h, 3.0EC, wird geblockt abgehalten
TUWEL

Merkmale

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

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage (u.a.)

  • fundamentale Prinzipien, Konzepte und Verfahren zur Programmanalyse und Programmverifikation, insbesondere von Korrektheit und Vollständigkeit am Beispiel axiomatischer Semantik, Datenflussanalyse, abstrakter Interpretation und Modellprüfung aufzuzeigen, zu erläutern und zu illustrieren.
  • diese Konzepte auf Methoden zur Programmtransformation/optimierung zu übertragen und anzuwenden.

  • Gemeinsamkeiten, Analogien und Unterschiede zwischen Programmanalyse und Programmverifikation zu verstehen und herauszuarbeiten.

  • die Möglichkeiten und Grenzen insbesondere automatischer und semi-automatischer Verfahren zur Programmanalyse, Programmverifikation und Programmtransformation/-optimierung im Spannungsfeld von Entscheidbarkeit, Skalierbarkeit, Wirksamkeit und Nützlichkeit zu erkennen, einzuschätzen und zu bewerten.

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
  • Sprache WHILE
  • Operationelle Semantik
  • Denotationelle Semantik
  • Axiomatische Semantik
  • Axiomatische Ausführungszeitanalyse

Teil II: Analyse und Verifikation

  • Programmanalyse
  • Reverse Programmanalyse
  • Parallele Programmanalyse
  • Programmverifikation vs. Programmanalyse

Teil III: Transformation und Optimalität

  • Chaotische Fixpunktiteration
  • Partiell tote und geisterhafte Anweisungen
  • Partiell redundante Anweisungen
  • Partiell redundante Ausdrücke
  • Transformationskombinationen
  • Konstantenanalyse auf dem Wertegraphen

Teil IV: Abstrakte Interpretation und Modellprüfung

  • Abstrakte Interpretation und DFA
  • Modellprüfung und DFA
  • Modellprüfung und abstrakte Interpretation

Teil V: Abschluss und Ausblick

  • Resümee und Perspektiven

Literaturverzeichnis

Anhang

  • Mathematische Grundlagen
  • Pragmatik: Flussgraphvarianten

Ausgewählte Leseempfehlungen

  • Beatrice Berard, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Peit, Laure Petrucci, Philippe Schnoebelen with Pierre McKenzie. Systems and Software Verification: Model-Checking Techniques and Tools. Springer- V., 2001.
  • Jacques Loeckx, Kurt Sieber. The Foundations of Program Verification. Wiley, 1984.
  • Flemming Nielson, Hanne Riis Nielson, Chris Hankin. Principles of Program Analysis. Springer-V., 2. Auflage, 2005.
  • Hanne Riis Nielson, Flemming Nielson. Semantics with Applications: An Appetizer. Springer-V., 2007.

Methoden

  1. Angeleitetes eigenständiges Erlernen und Einüben: Durch Vorträge und umgekehrtes Klassenzimmer angeleitetes eigenständiges Erlernen und Einüben der in den Lernergebnissen beschriebenen Fähigkeiten mithilfe zur Verfügung gestellter Lehr- und Lernunterlagen, Übungsaufgaben und weiterer nach Bedarf selbstgewählter Materialien aus ergänzend und vertiefend vorgeschlagenen Lehrbüchern, Tutorien und wissenschaftlichen Originalarbeiten.
  2. Vorbild- und rückmeldungsgeleitetes Lernen: Präsentieren, erläutern, begründen, vergleichen, wertend gegenüberstellen eigener und fremder Aufgabenlösungen aus sachlicher und fachlicher Sicht in Übungseinheiten.
  3. Selbsteinschätzungstests: Tests zur regelmäßigen Seibsteinschätzung und Selbstreflexion des bisherigen eigenen Lernfortschritts und Lernerfolgs.

Prüfungsmodus

Prüfungsimmanent

Weitere Informationen

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 Lernaktivitäten der Lehrveranstaltung
(die Angaben Teil I bis Teil V beziehen sich auf die entsprechenden Teile
der Lehrveranstaltungsunterlagen):

  • Angeleitete Lernaktivitäten (17.5h)
    • Vortrag: 12.0h (12 Einheiten * 1.0h)
    • Umgekehrtes Klassenzimmer: 3.0h (6 Einheiten * 0.5h)
    • Übungseinheiten: 2.5h (5 * Einheiten * 0.5h)
  • Eigenständige Lernaktivitäten (57.0h)
    • Selbstständiges Erarbeiten von Lernergebnissen: 35.0h (Vorschlag: Teil I/4.0h, Teil II/6.0h, Teil III/10.0h, Teil IV/10.0h, Teil V/4.0h, Teil VI/1.0h)
    • Speziell: Lösen der Übungsaufgaben: 20.0h (Vorschlag: 4 Angaben * 2.0h + 4 Angaben * 3.0h)
    • Vorbereitung auf die mündliche Prüfung: 2.0h
  • Mündliche Prüfung: 0.5h

Die Lehrveranstaltung beginnt mit Vorbesprechung und erster Vorlesung
am Mittwoch, den 04.03.2020, von 16:15 Uhr bis 17:45 Uhr im
Hörsaal EI3a, Elektrot.Institutsg., Gußhausstr. 25-29, 2. Stock.

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mi.16:00 - 18:0004.03.2020 - 11.03.2020EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Analyse und Verifikation - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.04.03.202016:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
Mi.11.03.202016:00 - 18:00EI 3A Hörsaal LVA 185.276 VU Analyse und Verifikation
LVA wird geblockt abgehalten

Leistungsnachweis

  • Acht beurteilte Abgaben von Übungsaufgaben.
  • Eine beurteilte 30-minütige mündliche Prüfung über Vorlesungs- und Übungsstoff.

LVA-Anmeldung

Von Bis Abmeldung bis
31.01.2020 01:00 13.03.2020 12:00 31.03.2020 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