Analyse und Verifikation
LVA 185.276, VU 2.0, ECTS 3.0, 2021 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: Online
Aufgrund geltender
COVID-19-Beschränkungen
sind Lehrveranstaltungen im
SS 2021 ausschließich online abzuhalten.
Das gilt auch für die Lehrveranstaltung
Analyse und Verifikation. Dabei wird angestrebt,
die aus der
Unmittelbarkeit von
Präsenzveranstaltungen resultierenden
Vorteile in Form
von
Echtzeitvideokonferenzen
als
Online-Veranstaltungsformat
möglichst
umfassend zu erhalten.
Veranstaltungstermine
Vorbesprechung und erster Vortrag finden am
Mittwoch, den 03.03.2021, 16:15 - 18:00 Uhr,
ausschließlich
online in Form einer
Echtzeitvideokonferenz statt.
Die Zugangsinformation
für die Videokonferenz ist am 01.03.2021 als TISS-Nachricht
versandt worden; sie findet sich auch auf dem Lehrveranstaltungsnachrichtenbrett
in TISS und im zugehörigen TUWEL-Kurs.
Alle Termine finden ausschließlich online in Form von
Videokonferenzen statt. Die Veranstaltungszeiten verstehen
sich dabei jeweils inclusive einer 15-minütigen Pause.
| Datum und Zeit
| Ort
| Thema Vortrag
| Thema umgek. Klassenzimmer/Übung
|
| Mi, 03.03.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil I, Kap. 1
(Leit- und Kontrollfragen I)
| n.a. / Vorbesprechung
|
| Mi, 10.03.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil I, Kap. 2, 3
(Leit- und Kontrollfragen II)
| Teil I, Kap. 1
|
| Mi, 17.03.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil II, Kap. 4
(Leit- und Kontrollfragen III)
| Übung
|
| Mi, 24.03.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil II/III, Kap. 5, 6
(Leit- und Kontrollfragen IV)
| Teil I/II, Kap. 2, 3, 4
|
| Mi, 14.04.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil III, Kap. 7, 8
Leit- und Kontrollfragen V
| Übung
|
| Mi, 21.04.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil III, Kap. 9
(Leit- und Kontrollfragen VI)
| Teil II/III, Kap. 5, 6, 7, 8
|
| Mi, 28.04.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil III, Kap. 10, 11
(Leit- und Kontrollfragen VII)
| Übung
|
| Mi, 12.05.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil IV, Kap. 12
(Leit- und Kontrollfragen VIII)
| Teil III, Kap. 9, 10, 11
|
| Mi, 19.05.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil IV, Kap. 13
(Leit- und Kontrollfragen IX)
| Übung
|
| Mi, 26.05.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil IV, Kap. 14, 15
(Leit- und Kontrollfragen X)
| Teil IV, Kap. 11, 12
|
| Mi, 02.06.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil V, Kap. 16, 17, 18
(Leit- und Kontrollfragen XI)
| Übung
|
| Mi, 09.06.2021, 16:15 - 18:00 Uhr
| Online (Video-Konferenz)
| Teil VI, Kap. 19
(Leit- und Kontrollfragen XII)
| 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, 12.03.2021, 12:00 Uhr, die Abmeldefrist am Fr, 26.03.2021, 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
- 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.
Unterlagen zu Vorlesung und Übung sind nachstehend zur
Verfügung gestellt.
Vorlesung
|
Inhalt
|
Folien
|
Hinweise
|
| Vorlesungsfolien
| Kap. 1 bis Kap. 21
Literatur, Anhänge
| pdf
| Stand: 09.06.2021.
|
| Vorbesprechung
| Motivation,
Organisatorisches
| pdf
| Stand: 03.03.2021.
|
Übung
|
Abgabetermin
|
Angabe
|
Hinweise und Bemerkungen
|
| 02.06.2021
| 16.06.2021
| Blatt 8.pdf
| Letztes Aufgabenblatt, Abgabefrist 2 Wochen!
|
| 19.05.2021
| 02.06.2021
| Blatt 7.pdf
| Abgabefrist 2 Wochen!
|
| 07.05.2021
| 19.05.2021
| Blatt 6.pdf
| Verlängerte Abgabefrist!
|
| 14.04.2021
| 28.04.2021
| Blatt 5.pdf
| Keine.
|
| 24.03.2021
| 21.04.2021
| Blatt 4.pdf
| Keine.
|
| 24.03.2021
| 14.04.2021
|
Blatt 3.pdf
| Keine.
|
| 10.03.2021
| 24.03.2021
| Blatt 2.pdf
| Keine.
|
| 03.03.2021
| 17.03.2021
|
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