TU Wien:Analyse und Verifikation VU (Knoop)

Daten

Vortragende	Jens Knoop
ECTS	3
Alias	Analysis and Verification (en)
Abteilung	Forschungsbereich Compilers and Languages
Letzte Abhaltung	2023SS
Sprache	Deutsch
Mattermost	analyse-und-verifikation • Register • Mattermost-Infos
Links	tiss:185276 , Homepage

Zuordnungen

Master Logic and Computation	Wahlmodul Programming Languages and Verification
Master Software Engineering & Internet Computing	Wahlmodul Computersprachen und Programmierung

Inhalt

SS11:

• Semantiken von Programmiersprachen
  • Operationelle Semantik
  • Denotationelle Semantik
  • Axiomatische Semantik
• WCET Erweiterung für Operationelle Semantik & Axiomatische Semantik
• Datenflussanalyse
  • Globalisierungsstrategien (Meet Over All Paths (MOP), Maximal Fixed Point (MaxFP))
  • Reverse Datenflussanalyse
  • Beispiele
• Programmtransformationen
  • ...
  • Partial Dead Code Elimination
  • Partial Redundant Assignment Eliminiation

Ablauf

Prinzipell gibt es wöchentlich Vorlesung, durch diverse Ereignisse kommt es im Durchschnitt aber auf ungefähr jede 2. Woche. Zum vorgetragenen Stoff werden Übungsblätter online gestellt, für die man eine Woche Zeit hat. Die Aufgaben können alleine oder zu zweit gelöst werden.

Benötigte/Empfehlenswerte Vorkenntnisse

Formales Denken (FMinf) schadet bestimmt nicht. Vor Halbordnungen sollte man auch nicht zurückschrecken.

Vortrag

Prof. Knoop hat einen sehr angenehmen Vortragsstil und ist auch darauf bemüht den eher trockenen Stoff, durch teils witzige Analogien zu vermitteln.

Übungen

Je nach Semester gibt es 6-8 Übungsblätter, die schriftlich (z.B. LaTeX) abzugeben sind. Während die Aufgaben gegen Anfang des Semesters noch relativ einfach sind (zirka halber Tag Aufwand), werden die Beispiele gegen Ende sprunghaft zeitintensiver. Als das in der Vorlesung angesprochen wurde, stellte sich heraus, dass der Professor zu viel Vorwissen erwartet hat und machte die Woche darauf eine Übungsstunde statt der Vorlesung, in dem die Beispiele von ihm durchgegangen wurden.

Prüfung, Benotung

Die Prüfung findet mündlich statt und dauert zirka eine halbe Stunde. Generell wird das Verstehen des Stoffes und größere Zusammenhänge erwartet (z.B. warum läßt sich das Verifizieren bei der Axiomatische Semantik nicht automatisieren?), Details sind dabei nicht so wichtig, schaden aber nicht. Sollte man etwas nicht wissen, so ist Prof. Knoop ebenfalls wieder bemüht die Schwierigkeiten aufzudecken.

Dauer der Zeugnisausstellung

• wurde noch am selben Tag ausgestellt (SS11, 6.7.2011)

Zeitaufwand

angemessen

Unterlagen

noch offen

• Materialien

Tipps

noch offen

Highlights / Lob

noch offen

Verbesserungsvorschläge / Kritik

noch offen

Materialien

Diese Seite hat noch keine Anhänge, du kannst aber neue hinzufügen.