PERSÉE is a project funded by the ACI «Sécurité Informatique» project from the french ministry of research.
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.
