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.

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

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Distance Learning

Lernergebnisse

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

  • fundamentale Prinzipien, Konzepte und Verfahren zur Programmanalyse und Programmverifikation, insbesondere Korrektheit und Vollständigkeit am Beispiel axiomatischer Semantik, Datenflussanalyse, abstrakter Interpretation und Modellprüfung aufzuzeigen, zu erläutern und wertend einzuordnen.
  • 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 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

Abhaltemodus: Online

Aufgrund geltender COVID-19 Beschränkungen und Weisungen von Rektorat und Studiendekanat vom 26.01.2021 und 30.01.2021 findet die Lehrveranstaltung 185.276 Analyse und Verifikation im SS 2021 ausschließlich online statt. Die Vorteile der Unmittelbarkeit von Präsenzveranstaltungen sollen dabei möglichst umfassend erhalten bleiben. Die Veranstaltung findet deshalb in Form von Echtzeitvideokonferenzen statt.

  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 bereit 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 geleiteten Übungseinheiten.
  3. Selbsteinschätzungstests: Tests zur regelmäßigen Seibsteinschätzung und Selbstreflexion des bisherigen eigenen Lernfortschritts und Lernerfolgs; Leit- und Kontrollfragen.

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 (ausschließlich online, 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 (Home Universitying, 57.0h)
    • Selbstständiges Erarbeiten von Lernergebnissen: 35.0h (Richtwert: 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 (Richtwert: 4 Angaben * 2.0h + 4 Angaben * 3.0h)
    • Vorbereitung auf die mündliche Prüfung: 2.0h
  • Mündliche Prüfung (ausschließlich online, Videopräsenz): 0.5h

Die Lehrveranstaltung beginnt mit Vorbesprechung und erster Vorlesung
am Mittwoch, den 03.03.2020, 16:15 Uhr bis 18:00 Uhr (einschließlich einer 15min Pause) via Zoom. Der Zoom-Link ist am 01.03.2021 per TISS-Nachricht ausgesandt worden; er findet sich auch auf dem Lehrveranstaltungsnachrichtenbrett in TISS und im zugehörigen TUWEL-Kurs.

Vortragende

Institut

Leistungsnachweis

  • Online/offline, ohne physische Präsenz: Acht beurteilte Abgaben von Übungsaufgaben.
  • Online, Videopräsenz: Eine beurteilte 30-minütige mündliche Prüfung über Vorlesungs- und Übungsstoff.

Weitere beurteilte Leistungsnachweise gibt es nicht.

Erforderliche technische Voraussetzungen: Stabiler Internetanschluss, internetfähiges Endgerät mit Audio/Video-Empfang und Übertragung.

LVA-Anmeldung

Von Bis Abmeldung bis
29.01.2021 01:00 12.03.2021 12:00 26.03.2021 23:59

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