SAFER : Safety and Sécurité Analysis via Formal and Efficient veRification

Manager : Kaïs Klai

The systems developed today are increasingly complex and their operation can have significant consequences on their environment, even irreversible: avionics, medical systems, etc. It is therefore essential to guarantee safe systems, whose operation has been verified before they are implemented. The writing of a formal specification not only allows a better understanding of the system studied, but also to formally prove, by an exhaustive verification, its correct operation, whatever the execution of the system.

Our activities are based on three main research themes :

– Design of formal specifications :
Developing specifications is a delicate task, and it is easy to make mistakes. The formal specification framework forces greater precision, and is here underlying work that chooses an expression in UML diagrams.

– Parametric, modular and distributed verification :
The design of new verification techniques to combat the combinatorial explosion problem is a major focus of our research.

– Software safety and security :
The analysis of concurrent programs is still in its infancy. We study different formalisms for modelling parallel recursive programs, and associated analysis techniques. We are also developing different models for malware detection and malicious behaviour discovery.

See the team report 2012-2017 for more detailed information.