Assistants de preuve : renforcer la position européenne via EuroProofNet

Fédérer une communauté de chercheurs en Europe

Lancée en novembre 2021, EuroProofNet, vient d’atteindre en ce début d’année sa vitesse de croisière. L’objectif de cette action du programme européen COST (European Cooperation in Science and Technology), dirigée par Frédéric Blanqui, chargé de recherche au sein de l’équipe commune Deducteam (Inria de Saclay – ENS Paris-Saclay - Université Paris-Saclay) du Laboratoire des Méthodes Formelles ? Fédérer une communauté de chercheurs en Europe s’intéressant à la vérification des programmes informatiques et aux systèmes de preuve numérique, avec pour finalité d’améliorer l'interopérabilité de différents outils et d’en faciliter l’utilisation en Europe et dans le monde.

Frédéric Blanqui, à l’origine du projet, a su réunir autour de cette problématique une large communauté scientifique : plus de 200 participants, représentant une trentaine de pays d’Europe. Dotée d’un budget de 150 000 euros pour sa première année (sur ses quatre ans d’existence au total), EuroProofNet permet de mener des activités de mise en réseau, comme l’organisation de conférences, de colloques, des visites scientifiques, des échanges entre chercheurs, etc.

Des assistants de preuve indispensables

Le champ de recherche de cette communauté revêt une importance scientifique et technique majeure car les systèmes de preuve sont indispensables à la validation des systèmes critiques ! Ceux-ci permettent ainsi de s’assurer du bon fonctionnement de programmes informatiques complexes, utilisées dans de nombreux secteurs : par exemple l’industrie aérospatiale (pour le guidage de lanceurs spatiaux), la santé (pour la fiabilité de dispositifs médicaux, en radiographie, cardiologie, etc.), la banque (pour la sécurité des systèmes de gestion de données ou le cryptage de transactions), l’énergie (pour le pilotage de centrales nucléaires), ou encore la cybersécurité.

Quel est le but de la vérification ? « La preuve démontre la validité d’un programme informatique ou d’un système électronique, que les concepteurs d’applications critiques cherchent à établir. Un système de preuve permet de montrer que les logiciels impliqués réalisent bien la tâche pour laquelle ils ont été conçus et donnent les résultats que l’on attend d’eux », résume Frédéric Blanqui.

Le chercheur précise : « Il existe deux types de systèmes de preuve. Pour des problèmes simples, des programmes spécifiques s’avèrent capables de détecter automatiquement des erreurs dans un code. Cependant, leur périmètre d’action est limité, et, pour des problèmes plus complexes, les preuves formelles de validité s’obtiennent ‘à la main’, à l’aide d’assistants de preuve ».

L’Europe très investie dans la recherche

L’Europe constitue, avec les États-Unis, l’un des principaux centres mondiaux de recherche et développement en matière d’assistants de preuve. Les équipes européennes sont particulièrement actives sur ce sujet, en constant développement en raison des demandes. Les logiciels comme Coq, développé par Inria, ou Isabelle, conçu au Royaume-Uni et en Allemagne, comptent parmi les assistants de preuve les plus utilisés par les informaticiens, auxquels s’ajoutent d’autres outils développés par différentes équipes.

Un système de preuve se fonde sur quelques axiomes (des énoncés considérés comme universels), assortis de règles de raisonnement, à partir desquelles s’énoncent, comme en mathématiques, des conclusions logiques. Les logiciels utilisent en outre des fonctions informatiques, disponibles dans des librairies spécifiques à l’outil. « Chaque assistant de preuve opère selon un système logique et informatique qui lui est propre et il existe parfois des incompatibilités entre les approches proposées par des outils différents » éclaire Frédéric Blanqui.

L’interopérabilité des assistants de preuve au cœur du projet

Comment garantir alors que les conclusions obtenues avec un assistant de preuve sur la validité ou la sécurité d’un programme soient fiables – c’est-à-dire qu’elles ne dépendent pas du système utilisé ? « On pourra par exemple réaliser des vérifications indépendantes avec des outils différents et renforcer la confiance en un système de preuve par confrontation de ses conclusions avec celles obtenues avec d’autres systèmes, répond Frédéric Blanqui. Pour cela, il faut pouvoir ’traduire’ les fonctionnalités d’un outil vers un autre ».

L’interopérabilité des assistants de preuve est donc au cœur d’EuroProofNet qui compte au total six groupes de travail, dédiés chacun à une thématique scientifique. Outre l'interopérabilité des systèmes de preuve, figurent ainsi la preuve automatisée, la vérification de programmes, le développement de bibliothèques de preuves formelles, le développement des techniques d’apprentissage automatique dans les preuves, et les recherches sur la théorie des types qui est à la base des assistants de preuve modernes.

Des ambitions scientifiques élevées

« Nous avons engagé les premiers échanges au sein du réseau d’EuroProofNet début février, avec une première réunion ‘hybride’, en raison du contexte sanitaire actuel, à Valence en Espagne, explique Frédéric Blanqui. D’autres réunions sont prévues cette année, dont une école d’été prévue en France à Nantes, à l’occasion de laquelle nous allons mieux faire connaître Dedukti, un langage développé chez Inria qui permet d’encoder différentes fonctionnalités des systèmes logiques de manière modulaire ».

EuroProofNet s’est donné des ambitions scientifiques élevées, comme celle de développer des outils de traduction entre systèmes de preuve ou d’aboutir à un standard européen. « L’action aura aussi d’autres résultats, comme celui de renforcer la position européenne, académique et industrielle, sur un marché stratégique émergent et économiquement dynamique », conclut Frédéric Blanqui.  

En savoir plus

• « Why join a COST Action ? » (en anglais), COST - European Cooperation in Science and Technology, 21/11/2018
• Les objectifs d’EuroProofNet (en anglais), EuroProofNet
• Un exemple d’assistant de preuve, Coq. En vidéo : « Coq : aspects pratiques de la théorie des types », Yves Bertot, InriaChannel, YouTube, 7/1/2019