News
20. August - Die Informationen auf dieser Seite sind noch vorläufig.
Organisation
Der Modulverantwortliche ist Prof. Dr. Roland Meyer. Die Veranstaltung wird zudem von Jan Grünke betreut. Der Übungsbetrieb wird von Jakob Tepe geleitet.
- Vorlesungstermin: Mi, 16:45 - 18:15
- Übungstermin: Do, 11:30 - 13:00
Um die Studienleistung zu bestehen, müssen Sie durch Abgabe der Übungsblätter mindestens 60 Prozent der Punkte erreichen.
Vorlesung
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
Skript
-
Programmanalyse
-
PredAbs1
Handschriftl. Notizen zu Prädikatenabstraktion
-
PredAbs2
Handschriftl. Notizen zu Prädikatenabstraktion
-
CEGAR
Handschriftl. Notizen zu CEGAR
-
Reach
Handschriftl. Notizen zu Erreichbarkeitsanalyse und Bounded Model Checking
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.
