Complex Systems Verification (CSV)

• Official homepage (with schedule)

Description

Formal methods for verification, such as model checking, provides techniques for automatically verifying that a (model of a) system satisfies a given property. This module studies such techniques for advanced families of models, e.g. having infinite state space and/or stochastic behaviours. Such models occur naturally in numerous situations: for instance for systems handling unbounded data or communication channels; or to model quantities such as time; or also to represent large networks of systems. This course will focus on different such classes of models, and on some associated verification techniques.

Keywords

Verification; formal methods; model checking; automata; logics;

Prerequisites

Good knowledge on finite automata, graph algorithms and complexity; Taking or having taken a course on finite-state verification would definitely help. The module MAD is a nice complement.

Content

The course will mainly focus on stochastic systems and real-time systems. For both of them, we will introduce classical families of models, and develop verification and abstraction techniques to check their properties. We will also focus on classes of parameterized models, used to represent (unbounded) networks of distributed systems.

Acquired skills

This course will provide students with solid knowledge of advanced verification techniques.

Teachers

Ocan Sankur and Nathalie Bertrand.