Theoretical Computer Science

Bäume, Ordnungen und Anwendungen 2015/2016

Neuigkeiten

Organisation

Vorlesungstermine:

• Vorlesung: Mo 17:15 - 18:45 in 34-420
• Übung: Do 17:15 - 18:45 in 34-420
• Vorlesung im KIS und im Modulhandbuch.

Prüfungsmodalitäten:

1. Es sind 60% der Übungsaufgaben mit einem Plus zu lösen (sinnvoll bearbeitet).
2. Es ist eine Aufgabe an der Tafel vorzustellen.

Vorlesungsaufzeichnungen

1. Verbände und der Satz von Knaster und Tarski (Woche 1)
2. Ketten und Monotone Frameworks (Woche 2, korrigierte Version)
3. Intraprozedurale Analysen (Woche 3, siehe Folien)
4. Intraprozedurale Analysen (Woche 4, siehe auch Folien)
5. Interprozedurale Analyse mit Procedure-Summaries (Woche 5)
6. Interprozedurale Analyse mit Procedure-Summaries und Call-Strings (Woche 6)
7. Galois-Verbindungen (Woche 7)
8. Konstruktion von Galois-Verbindungen und konkrete Semantik (Woche 8)
9. Abstrakte Semantik (Woche 9)
10. Prädikatenabstraktion (Woche 10)
11. Abstrakte Semantik zur Prädikatenabstraktion (Woche 11)
12. Abstraktionsverfeinerung (Woche 12)
13. Bisimulation (Woche 13)
14. CTL (Woche 14)

• Abgetippte Notizen von Jonathan Kolberg
Achtung: Diese Notizen werden z.T. direkt in der Vorlesung mitgeschrieben. Daher können sie Fehler oder Notationen enthalten, die in den handschriftlichen Notizen bereits korrigiert bzw. geändert wurden.

Exercises

Organisatorisches:

• Die Übungsblätter werden Dienstags Abends an dieser Stelle veröffentlicht.
• Abgabetermin ist jeweils Dienstag, 14 Uhr, in der darauffolgenden Woche.
• Der Abgabekasten befindet sich im Treppenhaus in Gebäude 34, neben Raum 34-404.1.
• Bitte geben Sie zu zweit oder zu dritt ab.

Übungsblätter:

• Blatt 1
• Blatt 2
• Blatt 3
• Blatt 4
• Blatt 5
• Blatt 6
• Blatt 7
• Blatt 8
• Blatt 9
• Blatt 10
• Blatt 11
• Blatt 12
• Blatt 13
• Blatt 14

Inhalt der Vorlesung

1. Termersetzung und Programmiersprachen
• Strukturierte operationelle Semantik (und Induktion)
• Konfluenz und Backtracking
• Terminierung und Wohlfundiertheit
2. Verbandstheorie und Statische Analyse
• Verbände
• Fixpunkte
• Statische Analyse
3. Baumautomaten und XML
• XML-Schema und Baumautomaten
• Abschlusseigenschaften
• Entscheidungsprobleme
• Gleichheit und Kardinalität

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 [E-Book]
• R. Berghammer: Ordnungen, Verbände und Relationen mit Anwendungen. Springer Verlag, 2012 [E-Book]
• G. Grätzer: General Lattice Theory. Birkhäuser, 2003
• G. Birkhoff: Lattice Theory. Providence, RI,1967