Le lundi 2 février prochain marquera le lancement opérationnel du laboratoire de recherche ProofInUse, fruit d’une collaboration étroite entre l’Inria, plus spécifiquement l’équipe de recherche Toccata spécialisée dans ...les spécifications formelles et les preuves assistées par ordinateur, et la société AdaCore, éditeur d'outils de développement pour les systèmes critiques. Objectif de cette structure : fournir des outils de vérification basés sur la preuve mathématique à des acteurs industriels dans le but de remplacer ou compléter des activités existantes de test tout en réduisant les coûts de vérification.

Ce laboratoire commun souhaite en d'autres termes proposer aux industriels des outils de vérification de leurs logiciels et par là-même démocratiser l'utilisation des techniques de preuve. Fondée sur la preuve mathématique, la technologie Spark, proposée par ProofInUse, a en effet pour but de remplacer et/ou d'enrichir les activités de test existantes en en réduisant significativement les coûts. Pour cela, deux axes de recherche sont privilégiés : faciliter l’utilisation des prouveurs automatiques et permettre à l’utilisateur d’aller au-delà de ce qui est possible avec la technologie Spark actuelle.

La création du laboratoire ProoofInUSe a été validée au début de l’année dernière par l’ANR (Agence nationale de la recherche). Afin de marquer ses début opérationnels, un colloque d’une journée aura lieu à Paris le 2 février prochain à l’hôtel Novotel Montparnasse (15^e arrondissement). Avec des interventions, entre autres, de Claude Marché de l’Inria et de Yannick Moy d’AdaCore, les deux directeurs du laboratoire ProofInUse. En fin de journée, une séance de questions-réponses aura lieu avec le comité scientifique et stratégique du  laboratoire au sein duquel des personnalités du CEA, d’Airbus Defence & Space et de Dassault Aviation seront présentes.

Les renseignements pratiques sur cet événement sont accessibles ici.