Langages, Modèle, et Vérification

Présentation - Membres Publications de l'équipe Projets de l'équipe Actualités de l'équipe

Since 2015, the overall objective of the Languages, Modeling, Verification (LMV) team is to advance the reliability and security of software, particularly but not exclusively, 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..

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 consider properties local to functions (function contracts) but also temporal properties and other high-level properties.

We rely on several branches of formal methods including, among others, deductive verification, the theoretical foundations of the semantics of programming languages, but also typing,  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.

Nombre de membres : 15