Aller au contenu principal

Évelyne Contejean : Éviter les bugs informatiques

Portrait de chercheur ou chercheuse Article publié le 10 novembre 2022 , mis à jour le 17 novembre 2022

Évelyne Contejean est directrice de recherche CNRS au Laboratoire méthodes formelles (LMF – Univ. Paris-Saclay, CNRS, ENS Paris-Saclay, CentraleSupélec, Inria). Elle est spécialiste de la démonstration automatique et des assistants à la preuve. Ce domaine de recherche de l’informatique s’attache à concevoir des outils performants pour déjouer en amont tous les bugs potentiels des objets de l’écosystème numérique.

Dès 2018, Évelyne Contejean s’implique ardemment dans la construction du Laboratoire méthodes formelles, dont elle devient la directrice-adjointe lors de sa création, en 2021. Ce laboratoire rassemble une cinquantaine de chercheuses et chercheurs permanents issus principalement du Laboratoire de recherche en informatique (LRI - CNRS, Univ. Paris-Saclay) et du Laboratoire spécification et vérification (LSV - CNRS, ENS Paris-Saclay). « Les méthodes formelles sont un ensemble de techniques qui analysent notre monde numérique, présente la chercheuse. Nous les utilisons pour apporter des garanties sur le bon fonctionnement et la fiabilité de différents objets informatiques : programmes, logiciels, protocoles, systèmes. » L’objectif est d’apporter « la preuve » en amont, autant que possible, qu’il n’y aura aucun bug pour éviter des échecs comme celui du lancement d’Ariane 5 en 1996, que les collègues d’Évelyne Contejean ont été appelés à analyser.

 

Réécriture et démonstration automatique 

Les preuves sur ordinateur font appel notamment à la logique et aux mathématiques « discrètes ». La réécriture est une méthode pour traiter l’égalité dans les preuves. C’est un modèle de calcul qui modélise en particulier les langages de programmation. Évelyne Contejean réécrit les équations mathématiques pour en déduire d’autres, avec l’objectif d’automatiser le processus. « Le principe est le suivant : quand je sais que deux expressions sont égales, je peux remplacer la "plus grosse" par la "plus petite", c’est-à-dire calculer partiellement dans une équation très compliquée. Les deux propriétés essentielles d’un "bon" système de réécriture sont la confluence, qui assure que toutes les façons de calculer donnent le même résultat, et la terminaison, qui garantit que le processus s’arrête en un temps fini. L’idée est de fournir à l’utilisateur final un outil qui va lui permettre, à partir de la description de son problème sous forme d’équations, d’appuyer sur un bouton pour obtenir un résultat dans un délai le plus court possible. »

 

La logique d’un parcours dédié à la preuve

Passionnée de mathématiques, Évelyne Contejean prépare les grandes écoles à Besançon et est reçue à l’ENS de Fontenay-aux-Roses en 1984. Elle y poursuit son parcours universitaire tout en préparant l’agrégation de mathématiques. En parallèle, la lecture du livre Gödel, Escher, Bach de Douglas Hofstadter lui révèle le monde de la logique. En 1988, son agrégation en poche, la jeune scientifique se tourne vers la recherche en informatique : elle effectue son stage de master 2 au Laboratoire de recherche en informatique à Orsay puis, grâce à une bourse, s’engage dans la rédaction d’une thèse sur la réécriture d’équations mathématiques, qu’elle soutient en 1992. 

Après un post-doc d’un an à l’Institut Max Planck à Sarrebrück, toujours dans le domaine de la démonstration automatique, elle est recrutée en 1993 comme chargée de recherche au CNRS. Elle obtient l’habilitation à diriger les recherches en 2014 et devient directrice de recherche en 2019.

 

Alt-Ergo ou la possibilité de faire ses preuves

En 2011, Évelyne Contejean et ses collègues mettent au point un nouvel outil en parvenant à prendre en compte des égalités non orientables dans les démonstrateurs de théorèmes SMT (satisfiabilité modulo théories). « Ce travail allait de la théorie jusqu’à la création d’un outil, Alt-Ergo, aujourd’hui utilisé pour faire des preuves dans de nombreux domaines. » Ces recherches sont d’ailleurs récompensées par le prix de l’Association européenne d’informatique théorique (EATCS), décerné par la fédération européenne ETAPS lors des conférences de la théorie et de la pratique du logiciel.

 

Terminer ou ne pas terminer

Au début des années 2000, des chercheurs et chercheuses en informatique de différents pays (France, Allemagne, Pays Bas, États-Unis) se livrent à des compétitions de terminaison de systèmes de réécriture par outils interposés : comme la réécriture remplace – en principe – de grosses expressions par de plus petites, il doit être possible de démontrer que le processus se termine. C’est le but des outils d’analyse automatique de terminaison. Mais une dizaine d’années plus tard, deux outils se contredisent. L’idée vient alors à Évelyne Contejean de garantir les résultats de ces outils. Se prenant au jeu, elle développe des preuves interactives de critères de terminaison dans l’assistant à la preuve Coq : « les preuves sont détaillées à l’extrême, chaque étape est explicitée et chaque preuve est revérifiée par ordinateur. Cette analyse très fine permet d’optimiser la preuve même si elle a déjà été démontrée auparavant avec un papier et un crayon ».

 

L’utilité des assistants à la preuve

Les assistants à la preuve fabriquent des preuves plus sûres et plus sophistiquées que celles des démonstrateurs automatiques. « Les preuves obtenues rapidement de façon automatique font appel à des théories relativement simples. Si nous souhaitons examiner des concepts plus compliqués, nous devons faire appel à l’intelligence humaine. » Ces preuves sont construites interactivement avec un ordinateur. « Une fois la preuve établie, les assistants à la preuve vérifient que nous avons bien analysé tous les cas et que nous ne sommes pas trompés dans les enchaînements logiques. »

Évelyne Contejean a ensuite l’idée d’appliquer les méthodes formelles à d’autres objets, comme par exemple les langages centrés données, la spécialité de sa collègue Véronique Benzaken, avec qui elle collabore depuis une dizaine d’années. « Selon les domaines de l’informatique, les résultats peuvent être plus ou moins étayés. Lorsqu’on utilise un assistant à la preuve, nous obtenons des garanties fortes. » Ces recherches s’inscrivent dans le projet DataCert, soutenu par l’ANR et qui prend fin en 2021.

 

Un compilateur certifié

Aujourd’hui, Évelyne Contejean travaille sur le développement d’un compilateur vérifié pour SQL (Structured Query Language), le langage le plus répandu de gestion des données. « SQL prend les requêtes d’un utilisateur pour les réécrire en un plan exécutable. Or, cette transformation n’est ni évidente, ni immédiate. Les moteurs SQL actuels ont un certain nombre de recettes pour assurer cette transformation, mais rien ne dit qu’elles soient correctes, hormis le fait qu’elles sont utilisées depuis longtemps », constate la chercheuse. Non seulement Évelyne Contejean vérifie formellement les transformations les plus connues mais elle en proposera aussi de nouvelles. « Le fait de rentrer de façon "intime" dans les preuves entraine une meilleure compréhension et la possibilité de les améliorer, de les simplifier ou de découvrir de nouveaux théorèmes. »

Au travers de ses recherches et de ses implications dans différentes structures (CoNRS, Comue Université Paris-Saclay, laboratoire), Évelyne Contejean apprécie au jour le jour la grande liberté de son métier tout en prônant une certaine vision de son domaine de recherche en informatique : « à l’instar de Galilée qui voulait étudier la nature avec les mathématiques, je propose d’étudier le monde numérique avec les méthodes formelles », conclut-elle.