Descriptif

Our society relies on software and hardware systems for both safety- and mission-critical applications (e.g., autonomous vehicles, control systems, device drivers, ...) in different domains (e.g., aerospace, avionics, medical devices, ...). However, designing correct and reliable systems is challenging due to the systems' complexity (e.g., system's size, concurrency, ...). Model Checking studies the theory and algorithms that automatically check if a system always behaves "as intended". Such algorithms are successfully used in real life to verify hardware (e.g., in companies designing hardware like Intel, ARM, Apple, ...) and software (e.g., at NASA, Microsoft, ...).

This course is an introduction to Model Checking and will explain how we can specify a system (e.g., a program, the design of a microprocessor, a distributed protocol) and its properties with a mathematical formalisms (e.g., logic) and how we can reason automatically about all the possible system's executions (e.g., to show that a program or the design of a microprocessor do not contain bugs).

At the end of the course, a student will be able to:

- Model discrete systems (e.g., programs) using formal languages to precisely define the system's executions.

- Express different system properties (e.g., safety, liveness) using temporal logic.

- Reason algorithmically about all the possible executions of a system, deciding if a system satisfies a property.

- Implement the basic model checking algorithms for discrete systems and temporal logic properties.

- Manipulate programmatically state machines, automata, and logical formulas.

- Recognize the challenges of (statically) checking a complex system.

The lectures cover the theoretical aspects of Model Checking, introducing the necessary background, algorithms, and proofs showing the correctness of the approaches. During the tutorials, the students will learn how to implement, in practice, such automated reasoning techniques.

The course focuses on the algorithms for discrete, finite-state systems. It is a starting point for model checking more expressive systems, such as infinite-state systems (e.g., real software), probabilistic systems, timed and hybrid systems (e.g., control systems), and machine-learning systems (e.g., neural networks). The course is also a starting point for exploring other problems in formal methods (e.g., automated program synthesis).