Prix de thèse du GDR GPL : des travaux sur la vérification formelle récompensés

Le GDR GPL organise chaque année ses journées nationales afin de réunir tous les acteurs de sa communauté. À cette occasion, un prix de thèse et des accessits au prix de thèse sont accordés, afin de récompenser une excellente thèse préparée au sein du GDR GPL et de promouvoir les travaux auprès de la communauté scientifique.
Le GDR GPL a décerné son prix de thèse 2024 à Xavier Denis, qui a réalisé son doctorat au Laboratoire méthodes formelles (LMF – CNRS/ENS Paris-Saclay/Université Paris-Saclay) . Deux accessits ont été remis à Sylvain Guérin, qui a réalisé sa thèse au Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC - ENIB/ENSTA Bretagne/IMT Atlantique/Université de Bretagne Occidentale/Université Bretagne Sud/CNRS), et Youcef Remil, qui l’a réalisée au Laboratoire d'informatique en images et systèmes d'information (LIRIS - CNRS/INSA de Lyon/Université Claude Bernard Lyon 1).

La thèse de Xavier Denis, encadrée par Jacques-Henri Jourdan, chargé de recherche CNRS au LMF et Claude Marché, directeur de recherche Inria au LMF, porte sur la vérification formelle des programmes en Rust.
La vérification de programmes cherche à garantir l'absence de bugs informatiques grâce aux mathématiques, mais ces outils ont longtemps eu du mal à gérer les pointeurs, des objets contenant l’adresse mémoire d’une donnée ou d’une fonction et qui permettent d'avoir accès à la couche basse de l'ordinateur. Ceux-ci sont pourtant essentiels dans les systèmes critiques et ce sont justement eux qu'on souhaite vérifier !
Pour résoudre ce problème, Xavier Denis a développé Creusot, un outil de vérification qui exploite les particularités du langage Rust. Celui-ci utilise le système de types de Rust pour simplifier l'analyse des pointeurs, permettant ainsi de vérifier des programmes bas niveau plus efficacement. La thèse de Xavier Denis explore les aspects pratiques et théoriques de Creusot, de son interface utilisateur jusqu'à ses fondements mathématiques. L'efficacité de l'outil a été prouvée sur divers algorithmes complexes. Ces travaux ouvrent la voie à une vérification plus fiable des programmes Rust, tout en restant accessible aux développeurs et développeuses.

La thèse de Sylvain Guérin, récompensée par l’un des deux accessits, s’intitule FML : un langage de fédération de modèles pour l’interopérabilité sémantique de sources d’information hétérogènes. Elle a été encadrée par Antoine Beugnard, professeur à l’École Nationale Supérieure Mines-Telecom Atlantique Bretagne Pays de la Loire, membre du Lab-STICC.
Dans sa thèse, Sylvain Guérin part du constat que la modélisation est une pratique universelle à la base de la pensée humaine pour concevoir, comprendre, calculer, analyser, communiquer. L’ingénierie dirigée par les modèles se propose de systématiser l’utilisation de modèles dans toutes les tâches liées au cycle de vie des systèmes et des logiciels. Très souvent, seuls les expertes et experts en modélisation sont en mesure de s’y atteler. Le doctorant propose de généraliser l’usage des modèles à tout le monde, en offrant la capacité d’interpréter tout artefact informatique (par exemple une feuille de calcul) comme un modèle et en permettant de connecter de nombreux modèles. Cette approche est basée sur un langage de modélisation appelé FML, principal contributeur à l'infrastructure logicielle Openflexo, qui est une implémentation de cette solution.

La thèse CIFRE1  de Youcef Remil, encadrée par Jean-Francois Boulicaut, professeur à l’INSA Lyon, membre du LIRIS, en collaboration avec Infologic, est lauréate du second accessit du prix thèse 2024 du GDR GPL. Son sujet concerne la recherche et le développement de nouvelles méthodes d’intelligence artificielle pour les opérations informatiques (AIOps) pour la maintenance prédictive d'un grand parc de serveurs d'applications.
Les systèmes informatiques modernes sont supervisés en tenant compte des défis de scalabilité, de fiabilité et d’efficacité. Les méthodes traditionnelles de maintenance logicielle, basées sur des tâches manuelles et des systèmes experts, atteignent leurs limites. L'AIOps émerge comme une solution innovante, combinant recherche et industrie pour exploiter l'intelligence artificielle dans la surveillance des systèmes et réduire les coûts. Cependant, des défis persistent : l'absence de terminologie unifiée, des modèles prédictifs souvent inefficaces en pratique ou la dépendance aux modèles opaques. Cette thèse aborde ces défis avec des solutions concrètes et innovatrices.