Objectives
The aim of this module is to introduce key concepts related to the formal verification of concurrent and distributed software.
Syllabus - The following aspects are addressed:
- Introduction, role of verification in the development process. Modelling of behaviour and formal semantics.
- Process Algebras and Labelled Transition Systems (LTS).
- Behavioural Properties (non determinism, deadlock, livelock, fairness, starvation, etc.)
- Remarkable equivalences and pre-orders: trace, testing, simulation, bi-simulation.
- Temporal logics (LTL et CTL) and Model Checking, Kripke structure, Buchi Automata, Fix point.
- Petri Nets, modelling of concurrency, synchronisation, conflict. Finiteness. Linear Invariants.
- Enseignant: Gérard Memmi
- Enseignant: Gilles Vignon
- Enseignant responsable de l'UE: Vadim Malvone