LMV is a team of the Laboratoire d’Informatique Fondamentale d’Orléans, Université d’Orléans.
Since 2015, the overall objective of the Languages, Modeling, Verification (LMV) team is to advance the reliability and security of software, particularly in the context of the Internet of Things (IoT). This objective is part of the general field of cybersecurity. We aim to ensure that the software involved satisfies critical properties either by construction by leveraging the design of libraries and programming languages, or by using formal methods.
We consider both so-called transformational programs—which terminate and produce a single result from input data—and reactive programs—which do not terminate and interact continuously with their environment and whose behaviors are characterized by temporal descriptions.
The programs we consider are embedded software whether they are applications, operating system components, security-critical modules, software dealing with the deployment, configuration and reconfiguration of distributed applications on the Internet of Things, as well as parallel programs for the analysis of massive data from the IoT.
We rely on several branches of formal methods including, among others, the theoretical foundations of the semantics of programming languages, typing, deductive verification but also rewriting systems, static analysis and the combination of techniques. In most of our work, we use the Coq proof assistant to generate certified code when relevant or, at least, to strengthen confidence in the results obtained, or to complement the use of other formal methods.
To carry out this programme, the LMV team relies on collaborations at the local, regional, national and international levels with universities, public institutions and companies. The team is also strongly involved in training by and for research: many students participate in our work.
Frédéric Dabrowski co-chairs the CLAP national working groupe and LMV members participate to the following working groups: LVP, YODA (GDR-GPL), MFS (GDR-Sécurité) and Scalp (GdR IM).