Adacore

ProofInUse est un laboratoire commun à l’équipe de recherche Inria Toccata, spécialisée dans les spécifications formelles et les preuves assistées par ordinateur, et à AdaCore, PME éditrice de logiciels spécialisée dans la fourniture d’outils de développement de logiciels pour les systèmes critiques.

Son objectif : proposer des outils de vérifications basés sur la preuve mathématique et de résoudre les difficultés qui limitent aujourd’hui son utilisation au niveau industriel.

La place des logiciels dans les systèmes critiques n’a cessé de croître depuis l’an 2000, à travers une multitude d’utilisations (transports, médecine…). Dans de nombreux domaines les failles logiciel peuvent avoir de graves conséquences, humaines ou financières. Pour asseoir la robustesse de ces applications, les méthodes formelles, telle que l’utilisation de la preuve, offrent des avantages financiers et de sécurité. L’utilisation de la preuve simplifie le processus de vérification et en minore le coût.

Le LabCom ProofinUse souhaite donc proposer aux industriels des outils de vérification de leurs logiciels et ainsi démocratiser l’utilisation des techniques de preuve . Fondée sur la preuve mathématique, la technologie Spark* proposée par ProofInUSe a pour but de remplacer et/ou d’enrichir les activités de tests existantes, en en réduisant significativement les coûts. Pour cela, deux axes de recherche sont privilégiés par le LabCom :

• 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.

• permettre à l’utilisateur d’aller au-delà de ce qui est possible avec la technologie SPARK actuelle

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.