Analyse und Verifikation
LVA 185.276, VU 2.0, ECTS 3.0, 2007 W
MSE/W

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

Haben Sie Interesse an einem geförderten Auslandsstudium?

Informationen zu Fördermöglichkeiten finden Sie hier.

 

Anmeldesystem freigeschaltet!

Das elektronische Anmeldesystem ist jetzt freigeschaltet. Sie können sich ab sofort bis zum 15. Oktober 2007 für die Teilnahme an der Lehrveranstaltung "Analyse und Verifikation" anmelden. Bis zum 29. Oktober 2007 können Sie sich gegebenenfalls auch wieder abmelden. Nach dem 29. Oktober 2007 gehe ich davon aus, dass Sie die Lehrveranstaltung fest in Ihren Stundenplan aufgenommen haben und sie erfolgreich bis zum Ende besuchen wollen.

Zum Anmeldesystem.

Inhalt

Im Mittelpunkt der Vorlesung stehen die Konzepte von Korrektheit, Vollständigkeit und Optimalität in

Ziele

Voraussetzungen

Sie sollten mitbringen: Eine perfekte Ergänzung in diesem Semester...

Lehrbehelfe

Während der Lehrveranstaltung werden die verwendeten Folien und Aufgabenstellungen für den Übungsteil wöchentlich an dieser Stelle zur Verfügung gestellt.

Folien vom Thema Verfügbare Formate (Folien pro Seite) Hinweise und Bemerkungen
21.01.2008
11. Vorlesungsteil
CM-Spezialitäten
und
Interprozedurale DFA
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Siehe auch ausgeteilten Umdruck.

Letzte Vorlesung.

14.01.2008
10. Vorlesungsteil
Reverse Datenfluss-
analyse
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Zur Ergänzung:

"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz

10.12.2007
9. Vorlesungsteil
Sparse Code Motion "1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Keine.

Veranstaltungs-
hinweis

 
Kolloquium,
Prof. Dr. E.-R. Olderog, 13.12.2007, 14:00 Uhr c.t.,
EI 5, Gußhausstr. 25-29
 

03.12.2007
8. Vorlesungsteil
Lazy Code Motion "1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Keine.
26.11.2007
7. Vorlesungsteil
Programmrepräsentationen; von Verifikation über Analyse zu Transformation und Optimierung "1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Keine.
19.11.2007
6. Vorlesungsteil
Datenflussanalyse
MFP, MOP,
Sicherheits-,
Koinzidenztheorem,
Tool-Kit-Sicht
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Veranstaltungs-
hinweis

 
Informatik-Kolloquium,
Sir Tony Hoare, 27.11.2007, 17:00 Uhr s.t.,
EI 9, Gußhausstr. 25-29
 
05.11.2007
5. Vorlesungsteil
Natürliche
und
denotationelle
Semantik, Fixpunktsatz und mathematische Grundlagen, WCET-Analyse
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Keine.
29.10.2007
4. Vorlesungsteil
Totale Korrektheit,
Korrektheit vs.
Vollständigkeit
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Keine.
08.&29.10.2007
3. Vorlesungsteil
Axiomatische
Semantik:
Beweisskizzen
vs. baumartiger
Beweisstil
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Besprechung
wird fortgeführt
am 29.10.2007.
08.10.2007
2. Vorlesungsteil
Fortführung von Vorlesungsteil 1,
insbesondere
SO-Semantik
von WHILE und
induktives
Beweisen
Siehe Vorlesungs-
teil 1&2 vom
01.10.2007.

Veranstaltungs-
hinweis

 
WIT-Kolloquium,
Gen.Dir.Brigitte Ederer, 15.10.2007, 17:00 Uhr s.t.,
EI 7, Gußhausstr. 25-29
 

01.10.2007
1. Vorlesungsteil
Die Sprache
WHILE, Syntax und Semantik von
Ausdrücken
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz
Besprechung
wird fortgeführt
am 08.10.2007.
01.10.2007
Vorbesprechung
Motivation und
Organisatorisches
"1 F/S".pdf
"1 F/S".pdf.gz
 
"4 F/S".pdf
"4 F/S".pdf.gz
 
"8 F/S".pdf
"8 F/S".pdf.gz

Übung
 
Aufgabenblatt vom
Abgabe Verfügbare Formate Hinweise und Bemerkungen
14.01.2008 21.01.2008 Blatt 8.pdf
Blatt 8.pdf.gz
Letztes
Aufgabenblatt.
10.12.2007 14.01.2008 Blatt 7.pdf
Blatt 7.pdf.gz
Keine.
05.12.2007 10.12.2007 Blatt 6.pdf
Blatt 6.pdf.gz
Keine.
26.11.2007 03.12.2007 Blatt 5.pdf
Blatt 5.pdf.gz
Keine.
19.11.2007 26.11.2007 Blatt 4.pdf
Blatt 4.pdf.gz
Keine.
08.11.2007 19.11.2007 Blatt 3.pdf
Blatt 3.pdf.gz
Keine.
29.10.2007 05.11.2007 Blatt 2.pdf
Blatt 2.pdf.gz
Keine.
08.10.2007 29.10.2007 Blatt 1.pdf
Blatt 1.pdf.gz
Keine.

Zeit und Ort

Die Vorbesprechung (und im Anschluss daran die erste Vorlesung) für das Wintersemester 2007/2008 findet am Montag, den 01.10.2007, von 16:15 Uhr bis 17:45 Uhr im Hörsaal 14 im Haupthaus am Karlsplatz 13, 1040 Wien, statt. Dieser Montagstermin und Ort ist auch der regelmäßige Vorlesungstermin und -ort. Die Anmeldung zur Vorlesung wird über ein elektronisches Anmeldesystem erfolgen. Dieses Anmeldesystem wird nach der Vorbesprechung über diese Webseite erreichbar sein. Der Anmeldezeitraum wird ausreichend lang sein und voraussichtlich bis zum Montag, den 22. Oktober 2007, dauern.

Anrechenbarkeit

Die LVA ist anrechenbar als Wahllehrveranstaltung im Masterstudium "Software Engineering & Internet Computing (MSE/W)"

Prüfungen

Die Prüfungen zur Lehrveranstaltung sind mündlich und werden voraussichtlich in der letzten Vorlesungswoche stattfinden. Andere Termine sind nach Absprache möglich.

Vortragender

Jens Knoop, Tel.: 58801-18510, E-mail: knoop@complang.tuwien.ac.at
Sprechstunde
wiederholte LVAs:
Fkt. Programmierung
Analyse u. Verifikation
Grundl. meth. Arbeitens
Sonstige
Schnellzugriff:
TUWIS++
voriges Semester
voriges Jahr
top | HTML 4.01 | last update: 2014-05-04 (Knoop)