Modeling and verification

General presentation

The "Modelling and Verification" axis is concerned with the modelling, verification and testing of complex IT systems. They develop rigorous methods to guarantee the proper functioning of systems. The axis represents the conjunction of three types of research activities:

A theoretical activity, consisting of specifying and studying various formalisms, making it possible to model critical systems and express the expected functionalities. These are systems with infinite and/or reactive states, in particular distributed, timed, probabilistic systems,
An algorithmic activity, developing tools for the analysis of critical systems: model-checkers and simulators. This activity goes from the design of algorithms to their implementation, and
A more pragmatic modelling activity, which takes place within the framework of collaborations and participation in industrial projects. For a long time limited to finite state space systems, this activity is being extended to infinite systems (cf. AltaRica), whether discrete or continuous (hybrid systems, stochastic systems).
Seminar

Working Group "Modelling and Verification", Thursday 11am - room 076 LaBRI

Contacts