Programmanalyse
Vorlesung im Wintersemester 2017/18
News
- 13. Februar
- Die genauen Prüfungstermine im Februar stehen fest. Sie wurden an die angemeldeten Personen verschickt. Falls Sie die Prüfung im Februar ablegen möchten, aber keine EMail erhalten haben, dann melden Sie sich bitte schnellstmöglich.
- 1. Februar
- Das freiwillige Übungsblatt zur CEGAR-Loop ist online.
- 23. Januar
- Die Vorlesung fällt heute (23.01) aus und es gibt diese Woche kein neues Übungsblatt.
- 20. Januar
- Prüfungsanmeldeformalitäten im Bachelor: laut Prüfungsamt bedarf es einem Antrag auf Import, um die Vorlesung im Bachelor einbringen zu können. Nach Absprache mit dem Prüfungsamt wird die Annahme solcher Anträge kulant behandelt und ist noch möglich (bitte möglichst zeitnah einreichen).
- 10. Januar
- Die korrigierten Prüfungstermine stehen fest.
- 12. Dezember
- Es gab einen Bug in Aufgabe 7.1. Das verbesserte Übungsblatt ist online.
- 8. November
- Die Übung findet ab jetzt in IZ-358 statt (nicht in IZ-160).
- 25. Oktober
- Es gab eine kleine Änderung bei Aufgabe 3 auf Übungsblatt 2.
- 18. Oktober
- Das erste Übungsblatt ist online. Es ist bis Mittwoch 25. Oktober 12 Uhr abzugeben.
- 4. Oktober
- Raumänderung! Die Vorlesung findet in IZ-358 statt (nicht in IZ-160).
- 2. Juni
- Alle Informationen auf dieser Seite sind derzeit noch vorläufig.
Organisation
- Die Vorlesung wird von Sebastian Wolff gehalten, betreut von Prof. Dr. Roland Meyer.
- Die Übung wird von Elisabeth Neumann gehalten.
- Eintrag im QIS: Vorlesung, Übung
- Vorlesungstermin: Dienstag, 16:45 - 18:15, Raum IZ-358
- Übungstermin: Donnerstag, 15:00 - 16:30, Raum IZ-160
Prüfungstermine
Es wird zwei Slots für Prüfungstermine geben:- Slot 1: 20.02.18/21.02.18
- Slot 2: 13.03.18/14.03.18
Vorlesungsnotizen
Zur Vorlesung gibt es Vorlesungsaufzeichnungen, sowie handschriftliche Notizen:
Als weitere Materialien verweisen wir auf die Vorlesungen Bäume, Ordnungen, und Anwendungen und Formale Grundlagen der Programmierung aus früheren Semestern.
Übungsblätter
Die Übungsblätter werden hier online gestellt. Bitte geben Sie in Gruppen von 2-3 Personen ab. Zur Abgabe Ihrer Lösungen dient eine Box neben Büro IZ-343 im Institut für Theoretische Informatik, Informatikzentrum, Mühlenpfordtstr. 23.
- Übungsblatt 1
- Übungsblatt 2
- Übungsblatt 3
- Übungsblatt 4
- Übungsblatt 5
- Übungsblatt 6
- Übungsblatt 7
- Übungsblatt 8
- Übungsblatt 9
- Übungsblatt 10
- Übungsblatt 11
- Übungsblatt 12 (freiwilliges Übungsblatt)
Modul
Um das Modul erfolgreich abzuschließen, sind zwei Leistungen zu erbringen:- Prüfungsleistung: Mündliche Prüfung in der vorlesungsfreien Zeit.
- Studienleistung: Sie müssen durch Ihre Abgabe der Übungsblätter mindestens 60 Prozent der Punkte erreichen, sowie eine der Aufgaben an der Tafel präsentieren.
Inhalte
Die Vorlesung behandelt die folgenden Themengebiete:-
Verbandstheorie und statische Analyse
- Verbände
- Fixpunkte
- Datenflussanalyse
-
interprozedurale Analyse
- funktionaler Ansatz
- Procedure Summaries
- Call Strings
-
Semantik
- operationell
- denotationell
- axiomatisch
-
Verfahren zur Verifikation
- Hoare Logik
- Verification Conditions
-
Abstrakte Interpretation
- Galois Verbindungen
- abstrakte Semantik
- Prädikatenabstraktion
- Abstraktionsverfeinerung
-
Nebenläufigkeit
- Hoare Logik
- Owicki-Gries
- Rely-Guarantee
- Concurrent Separation Logic
Literatur
- F. Nielson, H. R. Nielson, C. Hankin: Principles of Program Analysis. Springer-Verlag, 2005.
- U. P. Khedker, A. Sanyal, B. Karkare: Data Flow Analysis - Theory and Practice. CRC Press, 2009.
- H. Seidl, R. Wilhelm, S. Hack: Übersetzerbau - Analyse und Transformation. Springer-Verlag, 2010.
- R. Berghammer: Ordnungen, Verbände und Relationen mit Anwendungen. Springer Verlag, 2012.
- G. Grätzer: General Lattice Theory. Birkhäuser, 2003.
- G. Birkhoff: Lattice Theory. Providence, 1967.