M2 Course Proposal, ENS-Lyon

• Title: Logic, Automata and Games for Advanced Verification
• Lecturers: Matteo Mio and Denis Kuperberg.
• Period: from September 2018 to December 2018.
• Number of Lectures: 12, 2h long.

Short Description:

The field of verification is concerned with proving properties of systems, for instance in order to avoid bugs in software.
Typically, a specification is given in a logical formalism, together with the description of a system, and an algorithm must decide whether the system complies with the specification.
It is also possible to give only a specification, and ask the algorithm to build a system complying with it. This is called the Synthesis Problem.

In this course, we will explore such formalisms, and show how the wanted algorithms can be obtained thanks to constructions using different models of automata and games. We will focus in particular on formalisms able to express complex specifications such as probabilistic or quantitative requirements, or properties over branching models. The students will learn about classical results in this field, as well as current research and new frameworks.

Prerequisites: ideally the students need to have some basic knowledge on standard finite automata and regular languages. We will anyway provide some notes during the course to refresh these notions. The students are also supposed to have already been exposed to (first order and propositional) logic, be familiar with the meaning of the usual connectives (and, or, not, exists, forall).