Why3, la plateforme française de vérification des logiciels

Voiture autonome, aviation, ferroviaire… dans de nombreuses applications où la moindre défaillance pourrait provoquer une catastrophe, les programmes informatiques doivent être quasi infaillibles. C'est pourquoi ces logiciels, dits « critiques », ne sont pas seulement testés, ils sont « prouvés ». Quelle différence ? Un « test » permet de faire tourner le logiciel avec quelques données et de s'assurer que le résultat est bien celui espéré. La « preuve » vérifie que le programme fonctionne correctement en examinant son code source et en justifiant, à l'aide de formules mathématiques, chaque opération effectuée.

On a alors la quasi-certitude que le programme répondra aux attentes, quelle que soit la configuration initiale. « Avec, entre autres, l'utilisation croissante d'algorithmes complexes dans les systèmes critiques, dont des programmes d'intelligence artificielle, ce marché de la 'preuve' ne peut que s'étendre dans les prochaines années », estime Yannick Moy, ingénieur logiciel chez AdaCore, société parisienne spécialiste des outils de développement et de vérification des logiciels critiques.

Récompenses en série

Problème : réaliser une preuve avec un papier et un crayon est extrêmement long. « Dans les années 1990, la 'preuve' des 90.000 lignes de code informatique de la ligne de métro automatique n° 14 à Paris, avait occupé 16 ingénieurs pendant trois ans », rappelle Jean-Christophe Filliâtre, directeur de recherche du CNRS au Laboratoire de méthodes formelles (LMF), mixte avec l'université Paris-Saclay, l'ENS et l'Inria. Des chercheurs de l'équipe Toccata, dont il fait partie avec Andrei Paskevich, travaillent depuis vingt ans sur des plateformes facilitant l'automatisation complète ou partielle.

Leur petit dernier, Why3, utilisé, entre autres par AdaCore, accumule les récompenses. En 2019, K. Rustan M. Leino, l'un des pères de Boogie, un concurrent de Why3 développé chez Microsoft , et Jean-Christophe Filliâtre ont reçu le prix de la conférence Computer Aided Verification. En novembre 2020, Why3 a décroché le « coup de coeur académique » du Hub Open Source du pôle de compétitivité Systematic Paris-Region.

Enfin, en mars 2021, Jean-Christophe Filliâtre et Andrei Paskevich ont remporté, grâce à Why3, le concours VerifyThis où des binômes de chercheurs ou d'étudiants doivent prouver les propriétés d'algorithmes complexes.