Winter Term 2026/27
Formal Games
| Event Type: | Seminar |
|---|---|
| Target Group: | Master Computer Science |
| Scope: | 2 SWS / 3 ECTS |
| Events: |
Kickoff:
October 30th 2026, 13:00 – 14:00 in room 010 (ATIS) (building 50.34) |
| Event Number: | 2400094 |
| ILIAS Course: | Link |
| Lecturers: |
Prof. Bernhard Beckert |
| Registration: | Register via the Wiwi-Portal by 26th of October 23:55 |
| Allocation of Places: | Topics will be distributed at the kickoff event. Priority will be given on a FCFS basis, considering preferences from registration. |
| Prerequisites: | No formal requirements, but prior experience with program analysis, verification or automated reasoning is helpful. |
| Language: | English |
Topics:
The following list of topics will be extended in the near future. If you have any questions about topics or organization, please contact Mattias Ulbrich.
- Dependent Strategies in Alternating-Time Temporal Logic
1. Alternating-Time Temporal Logic with Dependent Strategies
2. Background Paper (Sections 1-4) - Program Equivalence via Game Semantics
1. Program Equivalence in a Simple Language with State
2. An Invitation to Game Semantics - Modelling Simultaneous Games in Dynamic Logic
1. Modelling Simultaneous Games in Dynamic Logic, Synthese 2008
- Game Semantics for Concurrent Separation Logic
1. A Game Semantics of Concurrent Separation Logic
2. An Asynchronous Soundness Theorem for Concurrent Separation Logic - Model Checking/Satisfiability using Focus Games
1. Focus Games for Satisfiability and Completeness of Temporal Logic, LICS 2001
Related: Practical Model-Checking Using Games, TACAS 1998 - Practical Reactive Synthesis
1. Synthesis of Reactive(1) Designs, VMCAI 2006
2. Synthesis for LTL and LDL on Finite Traces, IJCAI 2015 - Strategy logic : Logic that treats strategies in two-player games as explicit first-order objects
1. Strategy Logic - Comparing Programs with Games: Refinement Verification
1. Software Verification of Hyperproperties Beyond k-Safety, CAV 2022
2. Verifying Hyperliveness, CAV 2019 - Memoryless Determinacy for Parity Games
1. Tree Automata, Mu Calculus and Determinacy - Decidability of the Church Synthesis Problem
1. Church's Problem and a Tour through Automata Theory - Deciding Parity Games in Quasi-Polynomial Time
1. Deciding Parity Games in Quasi-Polynomial Time - Rabin's Theorem on the decidability of S2S
1. Decidability of Second-Order Theories and Automata on Infinite Trees
2. Trees, Automata and Games - Game-Theoretic Analysis of Information Leakage
1. Information Leakage Games: Exploring Information as a Utility Function
- Comparing Programs with Games: Algorithmic Game Semantics
1. Applying Game Semantics to Compositional Software Modeling and Verification, TACAS 2004