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: 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 (ausschließlich online): 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 (ausschließlich online): 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.

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.2021, 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.

• 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 (beiderseitiges Einverständnis vorausgesetzt, kann dieser Prüfungsteil durch eine entsprechende Präsenzprüfung ersetzt werden, sollten die jeweils geltenden COVID-Regelungen dies zulassen).

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.