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.

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.

Abhaltemodus: Grundsätzlich in Präsenz

Die Lehrveranstaltung 185.278 Analyse und Verifikation ist im SS 23 grundsätzlich als Präsenzveranstaltung geplant. Im Fall von im Semesterverlauf erneut schlagend werdender COVID-19 Beschränkungen wird die Veranstaltung online (Zoom) in Form von Echtzeitvideokonferenzen fortgeführt, damit auch im Fall einer solchen Umstellung die Vorteile der Unmittelbarkeit von Präsenzveranstaltungen möglichst umfassend erhalten bleiben.

1. Angeleitetes eigenständiges Erlernen und Einüben (grundsätzlich in Präsenz): 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 (grundsätzlich in Prüsenz): 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 (online und offline, ohne physische Präsenz): Tests zur regelmäßigen Seibsteinschätzung und Selbstreflexion des bisherigen eigenen Lernfortschritts und Lernerfolgs; zusätzlich Leit- und Kontrollfragen.

Die Lehrveranstaltung findet grundsätzlich in Präsenz statt.  Sollte dies im Lauf des Semesters aufgrund erneuter COVID-19 Beschränkungen nicht oder nicht länger möglich sein, wird die Veranstaltung online (Zoom) in Form von Echtzeitvideokonferenzen fortgeführt, damit auch im Fall einer solchen Umstellung die Vorteile der Unmittelbarkeit von Präsenzveranstaltungen möglichst umfassend erhalten bleiben.

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 (grundsätzlich in Präsenz, 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 (grundsätzlich in Präsenz): 0.5h

Die Lehrveranstaltung beginnt mit Vorbesprechung und erster Vorlesung
am Mittwoch, den 01.03.2023, 16:15 Uhr bis 17:45 Uhr, Seminarraum FAV 01 A.

• Online/offline, ohne physische Präsenz: Acht beurteilte Abgaben von Übungsaufgaben.
• Grundsätzlich in Prä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.

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.