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

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

Vorbesprechung und Anmeldung

Siehe auch Zeit und Ort.

Die Anmeldung zur Vorlesung erfolgt in diesem Semester über die Funktionalität von TUWIS++. Anmeldungen sind ab sofort bis zum Freitag, den 20.10.2006, möglich; Abmeldungen sind möglich bis zum Dienstag, den 31.10.2006, ebenfalls über TUWIS++.

Achtung: Terminverlegung

Um eine zeitliche Überschneidung mit der LVA 185.190 "Effiziente Programme" aufzulösen, wird die Vorlesung gegenüber dem ursprünglichen Termin um 105 Minuten auf Dienstag, 17:45 Uhr s.t. bis 19:15 Uhr im GM 4 Knoller-Hörsaal verlegt. Die neue 17:45-Zeit gilt erstmals am Dienstag, den 17.10.2006.

Aktueller Hinweis

Ab dem 24.10.2006 findet die Vorlesung an folgendem neuem Ort statt: Bibliothek E185/1, Argentinierstr. 8, 4. Stock.

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
30.01.2007
12. Vorlesungsteil
Erschöpfende vs.
anforderungsgetriebene
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
Letzter Vorlesungsteil
23.01.2007
11. Vorlesungsteil
Partielle Redundanz-
elimination:
BCM, LCM
und SpCM
"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
Achtung:
 
Abweichende Zeit
am 23.01.2007:
16:00 Uhr s.t. - 17:00 Uhr!
16.01.2007
10. Vorlesungsteil
DFA-Toolkit-Sicht,
Beispiele
"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.
09.01.2007
9. Vorlesungsteil
Datenflussanalyse
MFP, MOP,
Sicherheits-,
Koinzidenztheorem
"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.
12.12.2006
8. Vorlesungsteil
Von Verifikation
über Analyse
zur Transformation:
Optimierung,
Teil 2
"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
Andere Formate
nicht verfügbar.
05.12.2006
7. Vorlesungsteil
Von Verifikation
über Analyse
zur Transformation:
Optimierung,
Teil 1
"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
Andere Formate
nicht verfügbar.
28.11.2006
6. Vorlesungsteil
WCET-Analyse,
Nachträge zu
Verbänden
und CPOs,
Fixpunktsatz
"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.
07.11.2006
5. Vorlesungsteil
Natürliche
und
denotationelle
Semantik
"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.
31.10.2006
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
Aktualisiert am 07.11.2006.
24.10.2006
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
Keine.
17.10.2006
2. Vorlesungsteil
Fortführung von Vorlesungsteil 1,
insbesondere induktives
Beweisen
Siehe Vorlesungs-
teil 1 vom
10.10.2006,
erweitert und
ergänzt am
17.10.2006.

Veranstaltungs-
hinweis

 
Kolloquiumsvortrag,
Prof. Dr. Helmut Veith, 18.10.2006, 16:00 Uhr s.t.,
EI 5, Gußhausstr. 25-29
 

10.10.2006
1. Vorlesungsteil
Die Sprache
WHILE, Syntax und SO-Semantik
"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
Erweitert
und ergänzt
am 17.10.2006 und
am 30.10.2006.
04.10.2006
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
Veranstaltungs-
hinweise

 
Antrittsvorlesung,
Univ.Prof. Dr. Hannes Werthner, 09.10.2006, 17:00 Uhr s.t.,
EI 9, Gußhausstr. 25-29
 

Kolloquiumsvortrag,
Dr. David F. Bacon, 06.10.2006, 10:00 Uhr c.t.,
EI 5, Gußhausstr. 25-29
 

Übung
 
Aufgabenblatt vom
Abgabe Verfügbare Formate Hinweise und Bemerkungen
16.01.2007 23.01.2007 Blatt 9.pdf
Blatt 9.pdf.gz
Letztes
Aufgabenblatt.
10.01.2007 16.01.2007 Blatt 8.pdf
Blatt 8.pdf.gz
Keine.
05.12.2006 12.12.2006 Blatt 7.pdf
Blatt 7.pdf.gz
Keine.
28.11.2006 05.12.2006 Blatt 6.pdf
Blatt 6.pdf.gz
Keine.
07.11.2006 28.11.2006 Blatt 5.pdf
Blatt 5.pdf.gz
Keine.
31.10.2006 07.11.2006 Blatt 4.pdf
Blatt 4.pdf.gz
Keine.
24.10.2006 31.10.2006 Blatt 3.pdf
Blatt 3.pdf.gz
Keine.
17.10.2006 24.10.2006 Blatt 2.pdf
Blatt 2.pdf.gz
Keine.
10.10.2006 17.10.2006 Blatt 1.pdf
Blatt 1.pdf.gz
Keine.

Zeit und Ort

Die Vorbesprechung für das Wintersemester 2006/2007 findet am Mittwoch, den 04.10.2006, von 15:00 Uhr s.t. bis ca. 15:30 Uhr im FH HS4 statt. Die Vorlesung wird ab 10. Oktober 2006 jeden Dienstag von 16:30 Uhr bis 18:00 Uhr im GM 4 Knoller-Hörsaal am Getreidemarkt 9, 1060 Wien, stattfinden (detaillierter Lageplan) stattfinden. Ab 17.10.2006 wird der Vorlesungsbeginn auf 17:45 Uhr verschoben!

Die Anmeldung zur Vorlesung erfolgt in diesem Semester über die Funktionalität von TUWIS++. Anmeldungen sind ab sofort bis zum Freitag, den 20.10.2006, möglich; Abmeldungen sind möglich bis zum Dienstag, den 31.10.2006, ebenfalls über TUWIS++.

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)