Formal Methods Department#
Description#The genesis of the Department Formal Methods is related to several joint projects which have structured research at LORIA in Formal Methods and related topics. Ten years ago, these teams have been federated in a joint project called QSL Qualité et Sûreté du Logiciel and have developed short joint projects; moreover, seminars have been organised by members of this department. Very recently, the project QSL has been extended into another regional project called SSS for Sûreté et Sécurité des Systèmes and has integrated colleagues from the Automatic Control Laboratory and form the Mathematics Laboratory. Moreover, these teams are strongly related to shared common concepts, techniques and tools related to formal methods and the six teams (Carte, Cassis, Dedale, Pareo, Types, Veridis/Mosel) of the department 2 called Formal Methods work in the following themes:
- Logics: rewriting logics, classical and intuitionistic logics, modal and temporal logics, separation logics, substructural logics.
- Modelling Techniques and Methods (B, Event B, TLA+,. . . )
- Computability Models and Complexity: adverse computations, rewriting, analog and hybrid models of computation.
- 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, . . .
Finally, the department is an opportunity for improving the collaboration among researchers working on close topics and for providing a structure allowing the preservation of teams and the possibility of evolution or cooperation of teams. The department will encourage the cooperation of researchers in new projects proposals.