Sites Inria

English version

Partenariat Recherche-Industrie

Emmanuelle Perrot - 2/02/2015

ProofInUse : kickoff meeting

Après plusieurs mois de construction, le labcom ProofInUse prend toute sa dimension opérationnelle. C’est en effet aujourd’hui qu’est officiellement lancé le début des travaux de développement qui vont permettre de fournir des outils de vérification pour les systèmes critiques.

Nouveau laboratoire public/privé, ProofInUse est créé pour élaborer des outils de preuves mathématiques. En partie financé par le gouvernement français, et cogéré par Inria et AdaCore, le principal fournisseur de solutions logicielles pour le langage Ada, ProofInUse a pour but de répandre l’utilisation d’outils de preuves formelles. Ces outils complètent ou remplacent les activités existantes du développement logiciel tout en réduisant les coûts de vérification. Le thème du labcom ProofinUse s’inscrit dans l’une des priorités scientifiques du centre Inria Saclay - Île-de-France relative à la sûreté, sécurité et fiabilité pour les architectures, les logiciels et les données.

Le déploiement des techniques de preuve dans les projets industriels de développement logiciel permet d’accroître l’automatisation des activités de vérification, ce qui réduit les coûts et le temps de développement des logiciels critiques. ProofInUse se base sur la technologie SPARK pour le développement d’applications critiques, une technologie développée par AdaCore et Altran. ProofInUse va fournir un laboratoire pour la recherche sur les techniques de preuves, l’objectif étant que ces recherches permettent de répondre aux défis technologiques et scientifiques qui se posent. Les recherches vont notamment viser à faciliter l’utilisation de démonstrateurs automatiques et à étendre les capacités de SPARK pour vérifier des propriétés plus complexes.

« Les outils de vérification basés sur la preuve mathématique ont précédemment été développés au sein du monde académique, ils ont fait leurs preuves pour trouver des bugs dans des logiciels critiques complexes » dit Claude Marché, directeur de recherche Inria. « Grâce à notre collaboration avec AdaCore, ProofInUse permettra de continuer à développer ces techniques en les intégrant davantage dans les processus traditionnels de développement logiciel, pour s’assurer qu’elles peuvent être appliquées avec succès dans un contexte industriel ».

ProofInUse est né du partage des ressources et des connaissances entre AdaCore et l’équipe de recherche Toccata, spécialisée dans les techniques de preuves de programmes. Lors d’une précédente collaboration entre AdaCore et Toccata, la technologie Why3 de Toccata a été intégrée au cœur de la technologie SPARK d’AdaCore.

« Nous vivons dans un monde dans lequel les logiciels prennent chaque jour une place plus importante, où il devient toujours plus important que les programmes soient fiables, sûrs et sécurisés » dit Cyrille Comar, président d’AdaCore. « Développer les techniques basées sur la preuve formelle au sein de SPARK en veillant à les intégrer complètement avec d’autres techniques de vérifications telles que les tests est un grand pas pour réduire les coûts et la durée des activités de vérification sans perdre en sûreté. La collaboration public/privé au sein de ProofInUse va donner un nouvel élan pour diffuser plus largement les techniques de vérification basées sur la preuve et accroître l’utilisation industrielle de ces techniques, ce qui devrait bénéficier autant aux industriels qu’au grand public. »

Mots-clés : ProofInUse LabCom Inria Saclay Ile-de-France Adacore

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !