PERSÉE is a project funded by the ACI «Sécurité Informatique» project from the french ministry of research.

Project themes:

Project description:

The purposes of PERSÉE are to develop new techniques for the automatic verification of heterogeneous systems with variables ranging over different and unbounded domains.

Indeed, formal verification methods that allow to increase the safety and the security of critical computerized systems, rely upon the use of simple models. However, complex critical systems (e.g. protocols, supervisors, distributed algorithms) use unbounded data structures (e.g. counters, stacks, clocks, queues) that are out of the scope of classical model-checking techniques.

The goals of PERSÉE will be matched by producing simplified models with hetergeneous variables from more general models or programs on the one hand, and, by combining, unifying and adapting existing or emerging symbolic techniques on the other hand. The construction of simplified models (mainly extended automata) rely upon abstraction techniques that are partially automatic yet.

The members of PERSÉE are at the origin of several emerging symbolic techniques. We aim at implement these techniques in an integrated model-checking environment that will benefit from our experience from the development of the tools TReX, FAST and BLAST.


The “ACI PERSÉE” gathers researchers from 3 teams located in Bordeaux (LaBRI), Cachan (LSV) and Paris (LIAFA). Bold names indicate project leaders.

Jean-Michel Couvreur
Alain Griffault
Jérôme Leroux
Frédéric Herbreteau
Kaninda Musumbu
Grégoire Sutre
Quang Tran The
Aymeric Vincent
Eugene Asarin
Ahmed Bouajjani
Emmanuel Freund
Peter Habermehl
Yan Jurski
Mihaela Sighireanu
Sébastien Bardin
Nathalie Bertrand
Alain Finkel
Audrey Halbert
David Nowak
Philippe Schnoebelen

Plenary Meetings



Valid HTML 4.01! Valid CSS!