|
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Contact Jobs |
Seminar: Games in Verification and Synthesis
Topic Assignment and Seminar Schedule Games provide a powerful framework for reasoning about the interaction between the components of reactive systems, such as communication protocols and control systems. In this seminar, we will study game-theoretic methods that derive implementations from formal specifications (synthesis) and that prove that a given implementation satisfies a logical property (verification). In both cases, we view the interaction between a software component and its environment as an infinite game; verification then amounts to checking that the strategy represented by the program is winning; synthesis amounts to deriving a winning strategy from a logical description of the winning condition.
Related Course: AG&VThe AG&V lecture (Automata, Games, and Verification) covers background and additional topics related to the seminar. We recommend (but do not require) attending AG&V in parallel. Preliminary list of topics
Seminar (7 CP) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||