Projet ANR-14-LAB3-0007 – ProofInUse : Preuve en Œuvre (Intégration de la preuve dans le développement logiciel)
Programme : Laboratoires Communs organismes de recherche publics - PME/ETI - Vague 3 (LabCom - Vague 3) 2014
Année de financement : 2014
Coordinateur du projet : Monsieur Claude Marché (Institut National de Recherche en Informatique et en Automatique)
Partenaires : Inria Centre Saclay - Île-De-France
Montant : 300000.0 euros
Date de début : 2014
Durée : 36 mois
Résumé : L'objectif du Laboratoire Commun ProofInUse est de proposer aux industriels des outils de vérification basés sur la preuve mathématique, qui visent à remplacer ou complémenter les activités de tests existantes, tout en réduisant les coûts de vérification. ProofInUse est issu du partage de ressources et de connaissances entre l'équipe de recherche Toccata, spécialisée en techniques de preuve de programmes, et AdaCore, PME éditrice de logiciels spécialisée dans la fourniture d'outils de développement pour les systèmes critiques. Une précédente expérience réussie de collaboration entre Toccata et AdaCore a permis de mettre la technologie Why3 développée par Toccata au cœur de la technologie
SPARK développée par AdaCore.
Le but du Laboratoire Commun ProofInUse est d'augmenter notablement le nombre d'industriels clients de la technologie SPARK, en démocratisant l'utilisation des techniques de preuve. Cette démocratisation passe par la résolution de plusieurs verrous scientifiques et techniques :
Un premier axe de recherche et d'innovation consistera à faciliter l'utilisation des prouveurs automatiques. Il s'agira d'abord de fournir une meilleure interaction avec l'utilisateur, en particulier pour débugger les spécifications non prouvables, comme ce qu'il est coutume d'attendre d'autres activités de développement. Ensuite, le Laboratoire Commun aura 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 manipulation de données. En effet, l'intérêt économique des 
techniques de preuve repose pour une grande part sur leur automatisation, dont toute amélioration se traduira par une attractivité accrue de la technologie SPARK. Ces deux points nécessiteront des avancées scientifiques en termes de support à la génération de contre-exemples et de modélisation des types de données adaptée aux capacités intrinsèques des prouveurs automatiques.
Un second axe de recherche et d'innovation consistera à permettre à l'utilisateur d'aller au-delà de ce qui est possible avec la technologie SPARK actuelle, en termes de spécification des programmes et de preuves de ces spécifications. Du côté spécification, il s'agira de supporter des constructions plus complexes dans la technologie Why3, qui permettent d'étendre le langage de programmation inclus dans SPARK. Cela permettra en particulier de satisfaire les utilisateurs qui veulent spécifier des propriétés d'invariance des données manipulées. Du côté preuves, l'ambition du Laboratoire Commun est de donner la possibilité à l'utilisateur de guider la preuve des propriétés les plus complexes, celles qui résistent aux prouveurs automatiques. Ces deux points nécessiteront des avancées scientifiques au niveau des constructions du langage intermédiaire utilisé pour la preuve, ainsi que des méthodes de génération d'obligations de preuve, afin de permettre ces utilisations.
L’équipe de recherche Toccata est commune au centre Inria de Saclay et au Laboratoire de Recherche en Informatique (UMR Université Paris-Sud et CNRS). Cette équipe développe et distribue des logiciels pour la preuve de programme. L'équipe Toccata collabore depuis près de dix ans avec des industriels utilisateurs de ces outils, dont Airbus, Dassault-Aviation, Gemalto.
AdaCore est une PME internationale, avec un effectif partagé pour moitié entre l'Europe et les États-Unis. AdaCore développe et distribue des logiciels pour le développement de systèmes critiques, en particulier l'environnement de développement GNAT Pro pour le langage de programmation Ada. AdaCore collabore depuis 2008 avec le groupe Altran autour de la technologie de preuve SPARK.