Objectives
Model checking concerns the use of algorithmic methods for the assurance of software and hardware systems. As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a concern of overwhelming importance, and their reliability can no longer be sufficiently controlled by the traditional approaches of testing and simulation.

Syllabus
Verification algorithms: linear and branching temporal logics, omega automata, equivalences.
State explosion: symbolic data structures, automatic abstraction, compositional reasoning.
Case studies

Course structure
6 CFUs. Exam consists in an oral test and possibly of a small project.