Semantik SS25

News

• Übungen werden alleine oder in 2er Teams per Email abgegeben
• Die Übungen vom 1. Mai und Himmelfahrt (29. Mai) werden am Mittwoch den 30.4. bzw. 28.5. um 15 Uhr stattfinden
• 20. Februar: Die Informationen auf dieser Seite sind noch vorläufig.
• 20./21./23. Mai fällt Vorlesung/Übung aus
• In der Woche vom 7.-11.Juli fällt Vorlesung und Übung aus. In der darauffolgenden Woche ist die Übung am Dienstag (normaler Zeitslot) und die Vorlesung am Mittwoch (normaler Zeitslot)  und Donnerstag um 9.45. 
• Das aktuelle Blatt kann bis zum 24.07. abgegeben werden. Es wird auch noch ein Bonusblatt geben für die die eventuell noch Punkte brauchen. Das wird Anfang nächster Woche erscheinen.

Organisation

• Die Vorlesung hält Prof. Dr. Roland Meyer.
• Vorlesung: Dienstag 11:30 (IZ 358), Mittwoch 13:15 (IZ 358)
• Übung: Donnerstag 16:45 (IZ 358)
• Die Vorlesung beginnt am 15.04.

Lecture Notes

This lecture is a newly revised lecture. There is material from other courses that overlap thematically. However, this lecture is based on the handwritten notes taken during the semester.

• Overview, while programs, safety properties
• Abstract Interpretation
• Well-quasi orders & Upward-closed sets
• Well-structured domains, Abdulla's Backwards Search
• Predicate Abstraction 1, Predicate Abstraction 2, CEGAR
• IC3 Slides, Lattice Theoretic PDR
• Transition Invariants, Liveness, Transition Predicate Abstraction
• LTL 1, LTL 2
• Mu Calculus 1, Mu Calculus 2
• Algorithmic Aspects of WQO Theory, Applications of LFT, Proof of LFT 1, Proof LFT 2
  • Lecture notes from Schmitz and Schnoebelen
• Ordinals, Ordinals

Exercise Sheets

• Sheet 1
• Sheet 2
• Sheet 3
• Sheet 4
• Sheet 5, Project files
• Sheet 6
• Sheet 7
• Sheet 8
• Sheet 9, Solutions
• Bonus Sheet

Literature

The lectures will be based upon the following books and articles. Most of them are available online.

• Naoki Kobayashi, C.-H. Luke Ong: A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS 2009: 179-188.
• C.-H. Luke Ong: On Model-Checking Trees Generated by Higher-Order Recursion Schemes. LICS 2006: 81-90.
• B. Khoussainov, A. Nerode. Automata Theory and its Applications. Birkhäuser, 2001.
• M. Hofmann and M. Lange. Automatentheorie und Logik. Springer-Verlag, 2011.
• Th. Cachat. Symbolic Strategy Synthesis for Games on Pushdown Graphs. In Proc. of the 29th International Colloquium on Automata, Languages and Programming, ICALP, pages 704-715, Springer, 2002.
• I. Walukiewicz. Pushdown Processes: Games and Model Checking. In Journal Information and Computation - Special issue on FLOC '96, pages 234-263. Academic Press, 2001. Pages 234-263
• L. Holik, R. Meyer, S. Muskalla. Summaries for Context-Free Games. In Proc.of 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, pages 41:1-41:16. LIPIcs, 2016.
• O. Serre. Note on winning positions on pushdown games with omega-regular winning conditions. In Information Processing Letters, Vol 85 Issue 6, pages 285-291. Elsevier, 2003.
• D. A. Martin. A purely inductive proof of Borel determinacy. In Proc. Sympos. Pure Math., Vol 42, page 303-30. AMS, 1985.
• U. Zwick, M. Paterson. The complexity of mean payoff games on graphs. In Theoretical Computer Science, Vol. 158, Issues 1-2, pages 343-359. Elsevier, 1996.