Haben Sie Interesse an einem geförderten Auslandsstudium?

Informationen zu Fördermöglichkeiten finden Sie hier.

Vorlesungstermine

Di, 28.06.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Di, 21.06.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Di, 14.06.2016: Keine Vorlesung
Di, 07.06.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Di, 31.05.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Di, 24.05.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Mi, 18.05.2016, 17:00 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, Raumnummer CD0204.
Di, 17.05.2016: Keine Vorlesung (Pfingstferien)
Di, 10.05.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, Raumnummer CD0204.
Di, 03.05.2016: Keine Vorlesung
Di, 26.04.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Di, 19.04.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Freitag, 15. April 2016: Einladung zum Informatik-Kolloquium über Functional Reactive Programming for Real-Time and Cyber-Physical Systems: Response Time Analysis, Scheduling, and Verification von Prof. Dr. Albert M.K. Cheng, University of Houston, TX, um 14:15 Uhr im Hörsaal EI5 Hochenegg. Sie sind zu diesem Kolloquium herzlich eingeladen!
Di, 12.04.2016: Keine Vorlesung
Di, 05.04.2016: Keine Vorlesung (verlegt auf Mi, 18.05.2016)
Di, 29.03.2016: Keine Vorlesung (Osterferien)
Di, 22.03.2016: Keine Vorlesung (Osterferien)
Mi, 16.03.2016, 16:30 - 18:00 Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).
Di, 15.03.2016: Keine Vorlesung (verlegt auf Mi, 16.03.2016)
Di, 08.03.2016, 16:30 - 18:00 Uhr s.t., Seminarraum 125, Elektrot.Institutsg. (Gußhausstr. 25-29) - Stiege 1, 2. Stock, Raumnummer CD0204.
Di, 01.03.2016, 16:30 - 18:00 Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte): Vorbesprechung und erste Vorlesung.

AuV185.276-spezifische Vorbesprechung

Die spezielle Vorbesprechung für die LVA 185.276 "Analyse und Verifikation" findet zusammen mit der ersten Vorlesung am Di, den 01.03.2016, um 16:30 Uhr in der Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte), statt.

Anmeldung

Das elektronische Anmeldesystem ist offen bis zum 11. März 2016.

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
- Operationelle Semantik von WHILE
- Denotationelle Semantik von WHILE
- Axiomatische Semantik von WHILE
- Worst-Case Execution Time Analyse
Teil II: Analyse und Verifikation
- Programmanalyse
- Programmverifikation vs. Programmanalyse
- Reverse Datenflussanalyse
- Chaotische Fixpunktiteration
- Basisblock- vs. Einzelanweisungsgraphen
Teil III: Transformation und Optimalität
- Elimination partiell toter Anweisungen
- Elimination partiell redundanter Anweisungen
- Kombination von PRAE und PDCE
- Konstantenfaltung auf dem Wertegraphen
Teil IV: Abstrakte Interpretation und Modellprüfung
- Abstrakte Interpretation und DFA
- Modellprüfung und DFA
Teil V: Abschluss und Ausblick
- Resümee und Perspektiven

Voraussetzungen

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 "Optimierender Übersetzerbau", aber nicht zwingend erforderlich.

Abschlussprüfung und 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.

Vorlesungs- und Übungsunterlagen

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

Vorlesung	Inhalt	Folien	Hinweise
Vorlesungsfolien	Kap. 1 bis Kap. 17, Literatur, Anhang	pdf	Stand: 24.05.2016.
Zusatzmaterial	Hot-Spot Optimierer	pdf	Stand: 06.06.2010
Vorbesprechung (01.03.2015)	Motivation, Organisatorisches	pdf	Stand: 02.03.2016.

Übung	Abgabetermin	Angabe	Hinweise und Bemerkungen
31.05.2016	07.06.2016	Blatt 7.pdf	Letztes Aufgabenblatt.
24.05.2016	31.05.2016	Blatt 6.pdf	Keine.
10.05.2016	24.05.2016	Blatt 5.pdf	Keine.
26.04.2016	10.05.2016	Blatt 4.pdf	Keine.
19.04.2016	26.04.2016	Blatt 3.pdf	Keine.
15.03.2016	19.04.2016	Blatt 2.pdf	Keine.
08.03.2016	15.03.2016	Blatt 1.pdf	Keine.

Vortragender

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