Why3, lauréat du Prix Coup de Cœur Académique du Hub Open Source du Pôle Systematic

Paris, mercredi 18 novembre 2020

Rendez-vous incontournable de l’excellence scientifique et technologique de l’open source, la 5^ème édition de l’OSIS winter edition 2020 a eu lieu le mardi 17 novembre en webconference. Cet événement, organisé par le Hub Open Source du Pôle Systematic Paris-Region et l’Irill (Initiative de Recherche et Innovation sur le Logiciel libre) a réuni les chercheurs et ingénieurs des milieux académiques et industriels autour des projets de R&D les plus innovants.

C’est donc tout naturellement à cette occasion que le Hub Open Source a choisi de remettre pour la première fois son prix Coup de Cœur Académique !
En effet, avec ce prix coup de coeur académique, le Hub Open Source du Pôle Systematic a souhaité mettre en avant les projets académiques qui ont marqué les entreprises de l’Open Source.

Ce prix récompense un logiciel Open Source développé par un institut français d’enseignement supérieur et de recherche qui a influencé les industriels membres du Hub Open Source au cours de ces dix dernières années.
A travers ce prix, le Hub Open Source met à l’honneur l’excellence de la recherche universitaire et les collaborations entre les milieux académiques et industriels, dont la crise sanitaire a mis en lumière le rôle fondamental pour nos sociétés.
4 logiciels ont été présélectionnés par les experts du Hub Open Source sur la base des propositions faites par ses membres :

• OBP | ENSTA Bretagne
  Outil de vérification modulaire basé sur les observateurs répondant à la dynamique xDSL.
• Hardware Locality | Equipe-projet Tadaam, Inria Bordeaux – Sud-Ouest
  Logiciel utilisé pour connaître et abstraire l’architecture des ordinateurs.
• Why3 | Développé par l’équipe-projet commune “Toccata” du Centre Inria Saclay – Île-de-France et l’équipe Vals du LRI (Université Paris-Saclay et CNRS)
  Plateforme pour la vérification des programmes par preuve formelle.
• Scikit-Learn | Équipe projet Parietal, Inria Saclay – Île-de-France
  Bibliothèque libre Python destinée à l’apprentissage automatique.

Why3 est un environnement logiciel, dédié à la vérification de programmes, utilisant les techniques de preuve assistée par ordinateur à la pointe de la recherche académique. La plateforme fournit un langage riche pour la spécification et la programmation, appelé WhyML, et s’appuie sur des outils externes de preuve de théorèmes, soit automatiques soit interactifs, pour valider les conditions de vérification.

Cet environnement a fait l’objet de plusieurs activités de transfert vers le monde industriel, avec notamment :

• Le CEA-List (Saclay) qui développe l’environnement Frama-C pour la vérification de codes critiques écrits en langage C,
• Mitsubishi Electric R&D Centre Europe (Rennes) qui utilise Why3 pour des applications internes.

Le lauréat a reçu une dotation de 1.000€.
Dans une logique de contribution chère à l’écosystème, ce montant sera versé sous forme de donation à une association ou fondation à but non lucratif agissant pour l’Open Source de son choix.
L’équipe de Why3 a décidé de partager équitablement cette donation entre la fondation Wikimédia qui finance en particulier Wikipédia et Framasoft.