Theoretical Computer Science

Programmanalyse

Vorlesung im Wintersemester 2018/19

News

25. Januar

Die mündlichen Prüfungen werden voraussichtlich am 18/19/20 März stattfinden.

22. Januar

Das zwölfte und letzte Übungsblatt ist online.

21. November

Das vierte Übungsblatt ist optional: Die Punkte des Blattes sind Bonuspunkte zur Studienleistung.

02. November

Das zweite Übungsblatt ist online! Wir bitten den verspäteten Upload zu entschuldigen.

18. Oktober

In der ersten Vorlesungswoche (KW42) gibt es kein Übungsblatt und es wird keine Übung stattfinden.

11. Oktober

Die erste Vorlesung findet am 16.10 statt.

Organisation

• Die Vorlesung wird von Sebastian Wolff gehalten, betreut von Prof. Dr. Roland Meyer. Die Übung wird von Peter Chini gehalten.
• Eintrag im QIS: Vorlesung, Übung
• Vorlesungstermin: Dienstag, 16:45 - 18:15, Raum IZ-358
• Übungstermin: Donnerstag, 15:00 - 16:30, Raum IZ-358

Prüfungstermine

Vorlesungsnotizen

Zur Vorlesung gibt es Vorlesungsaufzeichnungen, sowie handschriftliche Notizen:

• Abstrakte Semantik
• Prädikatenabstraktion 1
• Prädikatenabstraktion 2
• Abstraktionsverfeinerung / CEGAR
• Erreichbarkeitsanalyse und Bounded Model Checking

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. Es gibt zwei Arten von Übungsblättern: theoretische und praktische. Theoretische Übungsblättern werden klassisch in Papierform abgegeben. Zur Abgabe Ihrer Lösungen dient eine Box neben Büro IZ-343 im Institut für Theoretische Informatik, Informatikzentrum, Mühlenpfordtstr. 23. Praktische Übungsblätter enthalten Programmieraufgaben. Diese werden digital abgegeben. Die genauen Modalitäten dafür werden noch bekannt gegeben.

Bitte geben Sie in Gruppen von 2-3 Personen ab.

• Übungsblatt 1
• Übungsblatt 2
• Übungsblatt 3
• Übungsblatt 4
• Übungsblatt 5
• Übungsblatt 6
• Übungsblatt 7
• Übungsblatt 8
• Übungsblatt 9
• Übungsblatt 10
• Übungsblatt 11
• Freiwilliges Übungsblatt 12

Modul

• Prüfungsleistung: Mündliche Prüfung in der vorlesungsfreien Zeit.
• Studienleistung:
  • Sie müssen durch Ihre Abgabe der theoretischen Übungsblätter mindestens 60 Prozent der Punkte erreichen, sowie eine der Aufgaben an der Tafel präsentieren.
  • Sie müssen durch Ihre Abgabe der praktischen Übungsblätter mindestens 60 Prozent der Punkte eines jeden Blattes erreichen.

Inhalte

• 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.