As computing systems become larger, more complex, and increasingly distributed and interactive, there is a pressing need for formal methods that guarantee their reliability, correctness, and efficiency. This network proposes a research and training programme for the design and verification of computing systems, using a methodological framework that is based on the interplay of finite and infinite games, mathematical logic and automata theory.
