Analyse und Verifikation
LVA 185.276, VU 2.0, ECTS 3.0, 2022 S

Analyse und Verifikation

(zweistündige Vorlesung mit Übung; siehe auch TISS/185.276)

Haben Sie Interesse an einem geförderten Auslandsstudium?

Informationen zu Fördermöglichkeiten finden Sie hier.

Abhaltemodus: Grundsätzlich Präsenz

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

Veranstaltungstermine

Vorbesprechung und erster Vortrag finden vorauss. am Mittwoch, den 02.03.2022, 16:15 - 17:45 Uhr.

Vortrag und umgekehrtes Klassenzimmer/Übung

Datum und Zeit	Ort	Thema Vortrag	Thema umgek. Klassenzimmer/Übung
Mi, 02.03.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil I, Kap. 1	n.a. / Vorbesprechung
Mi, 09.03.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil I, Kap. 2 - 3	Teil I, Kap. 1
Mi, 16.03.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil II, Kap. 4	Übung
Mi, 23.03.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil II/III, Kap. 5 - 6	Teil I/II, Kap. 2 - 4
Mi, 30.03.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil III, Kap. 7 - 8	Übung
Mi, 06.04.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil III, Kap. 9	Teil II/III, Kap. 5 - 8
Mi, 27.04.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil III, Kap. 10 - 11	Übung
Mi, 11.05.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil IV, Kap. 12	Teil III, Kap. 9 - 11
Mi, 18.05.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil IV, Kap. 13	Übung
Mi, 25.05.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil IV, Kap. 14 - 15	Teil IV, Kap. 12 - 13
Mi, 01.06.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil V, Kap. 16 - 18	Übung
Mi, 08.06.2022, 16:15 - 17:45 Uhr	EI 1 Petritsch HS	Teil VI, Kap. 19	Teil IV/V, Kap. 14 - 18

Terminänderungen werden hier bekanntgegeben. Die Teil- und Kapitelangaben beziehen sich auf die entsprechenden Teile und Kapitel der Lehrveranstaltungsunterlagen.

Anmeldung

Die Anmeldung zur Lehrveranstaltung über TISS/185.276 ist bereits möglich. Die Anmeldefrist endet am Fr, 11.03.2022, 12:00 Uhr, die Abmeldefrist am Fr, 25.03.2022, 12:00 Uhr.

Inhalt und Ziele

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 erstreckt sich dabei 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. Die Studierenden erhalten so in Theorie und Praxis ein profundes 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.

• 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

• Anhänge
  • Mathematische Grundlagen
  • Pragmatik: Flussgraphvarianten

• Ausgewählte Leseempfehlungen
  • Béatrice Bérard, Michel Bidoit, Alain Finkel, François 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.

Lehrveranstaltungs- und Übungsunterlagen

Lehrveranstaltungs- und Übungsunterlagen werden rechtzeitig im TUWEL-Kurs zur Lehrveranstaltung zur Verfügung gestellt.

Abschlussprüfung, Beurteilung, Gesamtnote

Die Abschlussprüfungen zur Lehrveranstaltung sind mündlich. Termine dafür werden individuell vereinbart und sollten im Regelfall Ende Juni, Anfang Juli stattfinden. Andere Termine sind nach Absprache möglich. Die Gesamtnote ergibt sich je zur Häfte aus Übungs- und Prüfungsnote.

Vortragender

Jens Knoop, Tel.: 58801-18510, E-mail: knoop@complang.tuwien.ac.at