Prüfungstermine
Die Prüfungen zur Vorlesung Semantik sollen am 15.09.2025 oder 16.09.2025 stattfinden.
Um einen Prüfungstermin zu vereinbaren, schreiben Sie eine Mail (ggf. mit Ihren zeitlichen Einschränkungen) an Jan Grünke.
Das genaue Datum und die Uhrzeit Ihrer Prüfung werden Ihnen dann zu einem späteren Zeitpunkt mitgeteilt.
Bitte beachten Sie, dass Sie sich unabhängig von der Vereinbarung eines Prüfungstermins beim Prüfungsamt/ im TUconnect-Portal für die Prüfung anmelden müssen!
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
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.