LMF - the new IT laboratory on campus!
The “Laboratoire méthodes formelles” (Formal methods laboratory) (LMF - Université Paris-Saclay, ENS Paris-Saclay, CNRS), which has resulted from the merging of two research groups, is today the leading authority in research into the safety and security of IT systems using mathematical tools. It aims to share its methods of analysis with other fields.
The “Laboratoire méthodes formelles” (LMF - Université Paris-Saclay, ENS Paris-Saclay, CNRS) was created on 1 January 2020. It is the result of merging the “Laboratoire spécification et vérification” (Specification and verification laboratory) (LSV - ENS Paris-Saclay, CNRS) with the VALS team (Vérification d'algorithmes, de langages et de systèmes - Verification of Algorithms, Languages and Systems) at the “Laboratoire de recherche en informatique” (Computer Science Research Laboratory) (LRI - Université Paris-Saclay, CNRS). Two secondary supervisors - Inria and CentraleSupélec - have been added to these three parent institutions. Led by Patricia Bouyer and her assistant, Évelyne Contejean, this new institution in Gif-sur-Yvette is the result of a restructuring of IT approved by the supervisory bodies in the spring of 2018 and validated by the High Council for the Evaluation of Research and Higher Education (Hcéres) during the five-year evaluation phase of public research laboratories. “The LSV and VALS team have already been working together for years, so this merger is very convenient. We are very pleased and excited about it because by bringing together the theoretical and applied aspects of our fields of study, we can share and foster new ambitious projects,” says Patricia Bouyer. The laboratory has one hundred full-time researchers, PhD students, post-doctoral students and support staff. It is structured around three hubs. Its main focus is divided into two areas – “Evidence” and “Models”, where methods of analysis, modelling and reasoning are developed for languages, programmes, protocols and computer systems. The third – “Interactions” - seeks to open up this research to other scientific fields. The three joint (EPC) Inria project teams Deducteam, Mexico and Toccata enhance this structure by having an adaptable approach linked to the EPC Inria model which promotes technological development and innovation.
The formal methods field of research
In computer science, formal methods are techniques which make it possible to use rigorous reasoning on computer programmes or systems in order to prove their conformity with expected performance. They use mathematical tools such as logic, automata, probabilities, topology and algorithms. Évelyne Contejean adds, “Our laboratory is at the point where computer science and mathematics meet. Galileo used the latter to study nature and we use it to decode the digital world.” The LMF’s key task is to manipulate these tools to develop methods for analysing computer programmes in order to guarantee their reliability and performance.
Recognition of the LMF by its professional peers
This field of research is very focused in terms of subject matter, but it covers all areas from theory to applications. This broad outlook is illustrated by the two Computer-Aided Verification (CAV) awards presented at the CAV international conferences. In 2017, Alain Finkel and Philippe Schnoebelen, researchers at the laboratory, received this prize for the development of mathematical structures leading to the general determinability of results for the verification of infinite transition systems. In 2019, Jean-Christophe Filliâtre (who also works at LMF) received his prize for the design and development of reusable intermediate verification languages, which have considerably simplified and accelerated the construction of automatic and practically usable deductive verification tools. “The LMF is one of the only laboratories in France and the world to have such strength amongst its researchers in the field of formal methods,” points out Evelyne Contejean.
Basic and applied research
Traditional applications of formal methods consist of guaranteeing the safety of software components used by stakeholders in highly sensitive sectors such as rail transport, aeronautics, aerospace, nuclear, defence and health. “A rocket exploding on launch or a cyber-attack are typically disasters related to problems of security or the operational safety of computer systems,” points out Patricia Bouyer. This guarantee that software components will function properly is of interest to industrialists, and the laboratory collaborates with many companies. Some examples are Alstom, Altran, Airbus, Dassault, Intel and Thales. Many of these companies are using software co-developed with LMF, which is TRL9 accredited (the Technology Readiness Level TRL is an ISO standard for measuring the level of technological readiness on a scale of one to nine) for research and development and production purposes, such as Why3, Alt-Ergo and HOL-TestGen. Others also benefit from these application solutions through the joint laboratory (Labcom) ProofInUse managed by EPC Inria Toccata from the LMF and the software publisher Adacore.
Sharing with other scientific fields
Bolstered by its success, the LMF is sharing its methods of analysis with other fields. For example, the laboratory has become involved in artificial intelligence, mainly through its participation in the neural network research project LeaRNNify, part of the European Procope cooperation programme with Germany. It has also started working in the field of quantum computing, because the new computing capacities offered by quantum mechanics require a review of all the traditional protocols, languages and verification techniques. There is also cybersecurity where performance guarantees are essential, particularly with regard to copyright protection, data confidentiality and privacy. The laboratory also draws inspiration from all these fields and uses their innovations to enrich its own range of techniques.
Story to be continued with the Laboratoire interdisciplinaire des sciences du numérique – LISN, unité de recherche du CNRS et de l’Université Paris-Saclay.