ProofInUse : le LabCom Inria-AdaCore

En janvier dernier, l'Agence nationale de la recherche (ANR) donnait son feu vert à la création de ProofinUse, le laboratoire créé conjointement par Toccata, une équipe Inria spécialisée dans les spécifications formelles et les preuves assistées par ordinateur et l’éditeur de logiciels AdaCore. Dans le même temps, ce Laboratoire commun (ou Labcom) bénéficiera d’un financement pendant trois ans. De quoi permettre aux deux partenaires de perfectionner les technologies qu’ils élaborent au service des entreprises. Cette nouvelle étape dans la collaboration entre Toccata et AdaCore vise à proposer aux industriels des outils de vérification des codes informatiques de leurs logiciels. Basée sur la preuve mathématique, cette méthode a vocation à remplacer ou à enrichir les activités de tests existantes, tout en réduisant les coûts de cette opération. La démocratisation de cette méthodologie passe cependant par la résolution de plusieurs verrous scientifiques et technologiques. Dans le cadre de ce LabCom, les deux partenaires entendent populariser auprès des industriels l’outil SPARK/Why3.
« Le financement accordé par l’ANR nous permet de recruter deux ingénieurs R&D de haut niveau, précise Claude Marché, responsable de l'équipe Toccata. L'ensemble des participantes et participants du LabCom sera en contact avec les clients de la technologie de preuve SPARK. »

Démocratiser l'utilisation des techniques de preuve

La structure ne cache pas ses ambitions.
« Un premier axe de recherche consistera à faciliter l'utilisation des prouveurs automatiques en fournissant une interface plus fonctionnelle, précise Yannick Moy, développeur pour AdaCore. Le LabCom aura ensuite comme objectif d'améliorer le ratio de prouvabilité des programmes couramment utilisés dans l'industrie, en particulier pour le calcul numérique et les manipulations de données. »

Le LabCom aura aussi pour objectif d’améliorer les capacités de ses outils. Ils seront ainsi plus efficaces, notamment dans les situations complexes où les prouveurs automatiques sont bloqués.

Toccata et AdaCore ont déjà collaboré sur le projet Hi-Lite, qui a permis d’intégrer la "la boite à outils" Why3 développée par Toccata , dans le logiciel SPARK développé par AdaCore  Ce travail commun a permis une nette amélioration des performances des chaînes de vérification et une réduction des risques d’erreurs lors du développement de logiciels embarqués. Par ailleurs, une thèse CIFRE, financée par l’éditeur AdaCore, est actuellement encadrée par Toccata. « Le recrutement par AdaCore de deux anciens doctorants de notre équipe a encore renforcé nos liens, précise Claude Marché. Du coté d’ AdaCore, ils sont très actifs pour promouvoir les approches par preuve de l'équipe Toccata. »