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

Analyse und Verifikation

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

Aktueller Hinweis: Aussetzung der Präsenzlehre an der TU Wien ab Mi, 11.03.2020 (COVID-19)!

Exzerpt von der TUW homepage: Ab Mittwoch, 11. März 2020 wird die Präsenzlehre an der TU Wien ausgesetzt, mit Montag, 16. März startet das Home Learning...

...die Präsenzlehre bleibt auch über Donnerstag, den 16.04.2020, hinaus ausgesetzt und wird aller Voraussicht nach auch in diesem Semester nicht wieder aufgenommen.

Für aktuelle weitere Hinweise und Informationen siehe COVID-19: Veranstaltungsabsagen und Verhaltenshinweise durch TU Wien (ursprünglich von Dienstag, den 10.03.2020.

Haben Sie Interesse an einem geförderten Auslandsstudium?

Informationen zu Fördermöglichkeiten finden Sie hier.

Veranstaltungstermine

Vortrag und umgekehrtes Klassenzimmer/Übung

Die Lehrveranstaltung beginnt mit Vorbesprechung und erstem Vortrag am Mittwoch, den 04.03.2020, 16:15 - 17:45 Uhr, im Hörsaal EI 3A, Elektrot.Institutsg., 2. Etage, Gußhausstr. 25-29.

Datum und Zeit	Ort	Thema Vortrag	Thema umgek. Klassenzimmer/Übung
Mi, 04.03.2020, 16:15 - 17:45 Uhr	Hörsaal EI 3A	Teil I, Kap. 1	n.a. / Vorbesprechung
Mi, 11.03.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil I, Kap. 2, 3	Teil I, Kap. 1
Mi, 18.03.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil II, Kap. 4	Übung
Mi, 25.03.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil II/III, Kap. 5, 6	Teil I/II, Kap. 2, 3, 4
Mi, 01.04.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil III, Kap. 7	Übung
Mi, 22.04.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil III, Kap. 8	Teil II/III, Kap. 5, 6, 7
Mi, 29.04.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil III, Kap. 9, 10	Übung
Mi, 13.05.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil IV, Kap. 11	Teil III, Kap. 8, 9, 10
Mi, 20.05.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil IV, Kap. 12	Übung
Mi, 27.05.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil IV, Kap. 13, 14	Teil IV, Kap. 10, 11
Mi, 03.06.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil V, Kap. 15, 16, 17	Übung
Mi, 10.06.2020, 16:15 - 17:45 Uhr Termin abgesagt durch TU Wien (COVID-19)	Hörsaal EI 3A	Teil VI, Kap. 18	Teil IV/V, Kap. 13 - 17

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

Anmeldung

Die Anmeldung zur Lehrveranstaltung erfolgt über TISS/185.276 und ist bis Fr, 13.03.2020, 12:00 Uhr, möglich.

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

Unterlagen zu Vorlesung und Übung sind nachstehend zur Verfügung gestellt.

Vorlesung	Inhalt	Folien	Hinweise
Vorlesungsfolien	Kap. 1 bis Kap. 18 Literatur, Anhänge	pdf	Stand: 22.06.2020.
Vorbesprechung	Motivation, Organisatorisches	pdf	Stand: 04.03.2020.   Termin und Ort von Vorbesprechung und erster Vorlesung: Mi, 04.03.2020, 16:15 - 17:45 Uhr, Hörsaal EI 3A, Elektrot.Institutsg., 2. Etage, Gußhausstr. 25-29.

 

Übung	Abgabetermin	Angabe	Hinweise und Bemerkungen
27.05.2020	10.06.2020	Blatt 8.pdf	Letzte Angabe, letzte SETs. SET 11 (27.05.2020) SET 10 (27.05.2020)
13.05.2020	27.05.2020	Blatt 7.pdf	SET 9 (11.05.2020)
30.04.2020	13.05.2020	Blatt 6.pdf	SET 8 (29.04.2020) SET 7 (22.04.2020) SET 6 (22.04.2020)
25.03.2020	22.04.2020	Blatt 5.pdf	SET 5 (25.03.2020)
18.03.2020	22.04.2020	Blatt 4.pdf	SET 4 (18.03.2020)
16.03.2020	22.04.2020	Blatt 3.pdf	SET 3 (16.03.2020) SET 2 (16.03.2020)
11.03.2020	22.04.2020	Blatt 2.pdf	SET 1 (11.03.2020)
04.03.2020	22.04.2020	Blatt 1.pdf	Keine.

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