The topic of the lecture is the verification of concurrent systems. We will study automata models for these systems (e.g Petri nets, WSTS, and distributed automata) and show how algorithmic problems for these models can be solved.
Traditionally, the contents of this lecture change every year. True to this spirit, the syllabus of this year's lecture will overlap, but not be same, as the one of the past four iterations of the lecture.
We plan to cover the following topics in detail:
- Petri nets: Reachability and coverability
- Well-structured transition systems
- Distributed automata
- Multi-pushdown automata
- TSO - A weak memory model for x86
You can find more details on these topics in the introduction of the lecture notes (to be uploaded soon).