The department Formal Methods focuses on methodologies, techniques and tools for analyzing, verifying and developing safe and secure software-based systems. The scientific directions of the department are organized as a triptych of three communicating and cooperating streams related to fundamental aspects and applications of formal methods:
- Logics, semantics and computability
- Formal system development
- Security and safety of software systems
The stream Logics, semantics and computability deals with fundamental aspects related to logic, proof theory, computability and complexity. The stream Formal system development concerns methodologies, techniques and tools for trustworthy software-based system development and the stream Security and safetyof software systems addresses the societal issues of security and trust.
The department consists of five teams sharing common concepts, techniques and tools related to formal methods and focusing on specific topics.
Research Domains
- Logics: rewriting logics, classical and intuitionistic logics, modal and temporal logics, separation logics, substructural logics.
- Modelling Techniques and Methods (B, Event B, TLA+,. . . )
- Virology
- Emerging computational models : quantum computing, higher-order computation, dynamical systems and computation with infinite precision
- Validation and verification for software-based systems
- Safety and security of systems
- Tools: proof assistant TLAPS, SMT solver veriT, the toolset EB2ALL, the toolset TOM, Virology-oriented tools, . . .
