Modern systems are increasingly complex, and their operation can have significant, and sometimes irreversible, consequences on their environment—such as in avionics or medical systems. It is therefore essential to guarantee safe systems whose behavior has been verified prior to deployment. Writing a formal specification not only leads to a better understanding of the system under study but also enables formal proof, through exhaustive verification, of its correct operation across all possible executions.
Our research activities are structured around three main themes:
- Design of Formal Specifications : Developing specifications is a delicate task, and errors are easily made. The framework of formal specifications demands greater precision and is fundamental to our work involving UML diagrams.
- Parameterized, Modular, and Distributed Verification : Designing new verification techniques to combat the state-space 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 various formalisms to model parallel recursive programs and their associated analysis techniques. We also develop different models for malware detection and the discovery of malicious behavior.
Consult the 2017–2022 team report for more detailed information.