Editing TU Wien:Analyse und Verifikation VU (Knoop)

== Daten ==
{{LVA-Daten
|ects=3
|vortragende=[[tiss.person:46163|Jens Knoop]]
|abteilung=Compilers and Languages
|homepage=http://www.complang.tuwien.ac.at/knoop/auv185276.html
|id=185276
|wann=SS
|alias=Analysis and Verification@en
|letzte_abhaltung=2022SS
|sprache=de
|mattermost=analyse-und-verifikation
|zuordnungen=
    {{Zuordnung|E066931|Programming Languages and Verification|wahl=1}}
    {{Zuordnung|E066937|Computersprachen und Programmierung|wahl=1}}
}}

== 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 ([[TU_Wien:Formale_Methoden_der_Informatik_VU_(Egly)|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

== Verbesserungsvorschläge / Kritik ==
noch offen

[[Kategorie:Theoretische Informatik und Logik]]