Programmanalyse
Vorlesung im Wintersemester 2023/2024
News
- 01. Februar
- Nächste Woche gibt es keine Übung. Falls dennoch Bedarf besteht (jemand z.B. am Mittwoch nicht zur Fragestunde kann) bitte melden, dann können wir doch noch eine Übung machen.
- 20. November
- Die erste Aufgabe von Blatt 4 wurde geändert.
- 17. November
- Hier ist ein Übungsvideo vom letzten Jahr: Video
- 15. November
- Die Übung am 16. November fällt aus. Stattdessen wird es ein Video geben. Das nächste Übungsblatt erscheint auch erst Freitag.
- 17. Oktober
- Die erste Vorlesung findet am 25.10.23 statt. Die erste Übung am 02.11.23.
Organisation
-
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.
- Die Vorlesung wird von Anton Opaterny, Jan Grünke, und Sören van der Wall gehalten, betreut von Prof. Dr. Roland Meyer. Die Übung wird von Jakob Tepe gehalten.
- Eintrag im QIS: 4212580
- Vorlesungstermin: Mittwoch, 9:45 - 11:15, Raum IZ 358
- Übungstermin: Donnerstag, 16:45 - 18:15, Raum IZ 358
Prüfung
Nach der Vorlesungszeit wird eine mündliche Prüfung abgehalten. Die Prüfungsmodalitäten werden zeitnah bekannt gegeben.
Vorlesung
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.
- Verification Conditions
- Galois Verbindungen 1
- Galois Verbindungen 2
- Abstrakte Semantik
- Prädikatenabstraktion 1
- Prädikatenabstraktion 2
- Abstraktionsverfeinerung / CEGAR
- Erreichbarkeitsanalyse und Bounded Model Checking
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
- Anwendungen
- CEGAR - CounterExample-Guided Abstraction Refinement
- BMC - Bounded Model Checking
Übungsbetrieb
Die Übungsblätter werden hier donnerstags online gestellt. Die Abgabe erfolgt per Email an Jakob Tepe. Die Abgabe erfolgt in Gruppen von 2 Personen, wie bei der ersten Vorlesung eingetragen. Bei Fragen zu oder Problemen mit den Übungen wenden Sie sich bitte an Jakob Tepe.
| Übungsblatt | Ausgabe | Abgabe |
| 1 | 26. Oktober | 01. November |
| 2 | 02. November | 08. November |
| 3 vcgen.cpp | 10. November | 15. November |
| 4 | 17. November | 22. November |
| 5 | 23. November | 29. November |
| 6 | 01. Dezember | 06. Dezember |
| 7 | 07. Dezember | 13. Dezember |
| 8 | 15. Dezember | 20. Dezember |
| 9 | 21. Dezember | 10. Januar |
| 10 | 11. Januar | 17. Januar |
| 11 | 18. Januar | 24. Januar |
| 12 | 25. Januar | 31. Januar |
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.