Vérification de logiciels critiques : création du laboratoire ProofInUse
Le lundi 2 février verra le lancement du laboratoire ProofInUse. Son objectif est de fournir des outils de vérification de logiciels basés sur la preuve mathématique à des acteurs industriels. Ces outils visent à remplacer ou à complémenter les activités existantes de tests, tout en réduisant les coûts de vérification pour l’aérospatial, le transport, la médecine ou encore l’aéronautique.
« Les logiciels vérifiés avec ces techniques formelles seront plus fiables et moins coûteux à développer », promettent les responsables du laboratoire.
C’est en 2014 que l’Agence Nationale de la Recherche (ANR) a validé le projet de laboratoire commun ProofInUse d’Inria, établissement public de recherche dédié aux sciences du numérique, et de la société AdaCore, éditeur de logiciels spécialisé dans la fourniture d’outils de développement et de vérification pour les logiciels critiques.
« La place des logiciels dans les systèmes informatiques, ainsi que leur criticité, ne cesse de croître dans tous les domaines. Pour certains, où la certification de ces systèmes est requise tels que l’aérospatial, le transport, la médecine ou encore l’aéronautique, la moindre faille logicielle peut avoir des conséquences dramatiques, tant humaines que financières. L’objectif de ce laboratoire commun, démontrant l’excellence de la recherche française, est d’augmenter le nombre d’utilisateurs industriels en démocratisant l’utilisation des technologies de preuve formelle », souligne le communiqué de ProofInUse.
