Why3, le programme qui vérifie les programmes

Quand sait-on qu’un programme est terminé et fonctionne correctement ? Plutôt que d’effectuer quelques tests à la main, différents outils permettent de s’assurer que le programme tourne, dans toutes les circonstances, comme prévu : on parle alors de vérification des programmes. Parmi ces options, la plateforme Why3 a été conçue par des chercheurs1 de l’équipe-projet Inria Toccata au sein du Laboratoire Méthodes Formelles et du CEA-LIST, et multiplie récompenses et partenariats industriels.

« La vérification déductive des programmes opérée par Why3 consiste à vérifier certaines propriétés d’un code, exprimées dans un langage mathématique rigoureux, détaille Jean-Christophe Filliâtre, directeur de recherche CNRS au LMF. On pense d’abord à regarder que le programme s’exécute correctement et ne risque pas de planter, par exemple à cause d’une division par zéro, mais les possibilités sont beaucoup plus nombreuses. Dans l’exemple d’un programme chargé de trier des données par ordre croissant, on va vouloir s’assurer qu’il rend le résultat bien ordonné, mais aussi qu’il ne perde ni n’ajoute de chiffres dans la manœuvre. »

L’outil de vérification analyse le code et sa spécification afin de produire une liste des énoncés mathématiques à démontrer, ce qui peut être accompli de deux manières. Certains assistants à la démonstration sont entièrement automatisés, mais, pour des preuves plus complexes, d’autres fonctionnent en interaction avec l’informaticien. Ce dernier va alors guider l’assistant afin de construire la preuve « à la main ». Why3 se distingue de la concurrence par sa capacité à assembler ces deux approches, ainsi qu’à cumuler le travail de plusieurs assistants à la fois, même s’ils reposent sur des systèmes différents. Tous ces éléments n’ont pas forcément été conçus par des chercheurs du LMF, mais Why3, qui est un logiciel libre, les combine harmonieusement sous une interface commune.

• 1Jean-Christophe Filliâtre, directeur de recherche CNRS, Claude Marché, directeur de recherche Inria, Guillaume Melquiond, chargé de recherche Inria, Andrei Paskevich, maître de conférences Université Paris-Saclay, membres de l'équipe-projet Inria Toccata au sein du LMF, et François Bobot, ingénieur-chercheur au CEA-LIST.

Why3 s’est illustré en mars dernier lors de la compétition VerifyThis. Depuis 2011, ce concours demande à des binômes de chercheurs, ou d’étudiants, de vérifier les propriétés d’algorithmes complexes. Ils peuvent utiliser les outils de leurs choix, si bien que quatre équipes sur vingt-trois ont choisi de passer par Why3. Résultat, le duo Jean-Christophe Filliâtre et Andrei Paskevich a remporté le concours, tandis que deux doctorants du LMF sont arrivés premiers ex-æquo avec une autre équipe dans la catégorie Étudiants. Un excellent palmarès, d’autant que l’édition 2021 était plus difficile et longue que d’habitude afin de compenser le fait qu’elle se tenait en distanciel.

En novembre 2020, Why3 avait également obtenu le prix du « Coup de cœur académique » du Hub Open Source du pôle Systematic, l’écosystème deep-tech de la région parisienne. Fidèle à l’éthique du logiciel libre, l’équipe a partagé la dotation de mille euros entre la fondation Wikimédia et l’association d’éducation populaire numérique Framasoft.

Une approche qui n’empêche pas pour autant Why3 d’opérer des transferts industriels. Par exemple avec le LIST de CEA Tech, qui mène des programmes de R&D dédiés aux systèmes numériques intelligents, pour le développement d’un environnement consacré à la vérification de codes écrits en langage C. L’équipe travaille également avec l’entreprise AdaCore et le centre européen de R&D de Mitsubishi Electric. L’écosystème trouve aussi le succès auprès du monde académique, en particulier dans des domaines tels que la cryptographie ou les contrats numériques.