Accueil

De CeProMi.

Bienvenue sur le site de l'ARC CeProMi

CeProMi est une Action de Recherche Coopérative (ARC) de l'INRIA.

Cette action se place dans le contexte de la spécification formelle et de la preuve de comportement de programmes, pour des programmes requérant un haut niveau de confiance. Elle vise à fédérer les efforts de quatre équipes françaises, dont trois équipes INRIA, sur les propriétés de programmes mettant en jeu du partage de la mémoire et des effets de bords : typiquement les données avec pointeurs en langage C, les objets en Java ou C++, les enregistrements avec champs mutables en ML. Le cas de ML introduit spécifiquement le problème du support des fonctions d'ordre supérieur.

Les axes d'étude envisagés correspondent à deux défis:

  1. Raisonner sur des programmes fonctionnels mettant en jeu à la fois de l'ordre supérieur et des effets de bords.
  2. Raisonner sur des programmes impératifs ou à objets, pour lesquels on souhaite encapsuler les effets des modules (c.-à-d. où les effets de bords de l'implantation d'un module sont invisibles dans l'interface)


L'objectif premier de l'action proposée est la mise en place d'outils théoriques pour surmonter ces défis. Les méthodes envisagées vont typiquement allier

  1. Une méthodologie (ou un langage) de spécification. Il faudra définir des politiques de modularité et de raffinement de spécification, des notions appropriées d'invariants, des systèmes d'annotations ou de description abstraite des effets de bords.
  2. Des systèmes de typage ou plus généralement des analyses statiques : analyse d'alias de pointeurs, de séparation des accès mémoire, etc.
  3. Des calculs d'obligations de preuve : plus faibles préconditions, conditions de raffinement.

Ces méthodes seront mises en application par des implémentations au sein de la plateforme Why de preuve de programmes, développée dans l'équipe INRIA ProVal ; puis par des études de cas. Les études de cas seront a priori de nature académique, mais avec pour objectif à plus long terme (en dehors de cette action) d'appliquer ces méthodes à des programmes de type embarqué en C, C++, Java(Card), dans des domaines critiques: avionique, automobile, cartes à puces; avec des partenaires industriels avec lesquels nous collaborons par ailleurs.

Outils personnels