Sous-projet 4 : Greffons de preuve automatique

Description du sous-projet, responsable, partenaires

Collaboration des outils de preuve.

Début : M1

Fin : M36

Responsable : INRIA

Participants : INRIA, CEA

Objectifs du sous-projet

Le premier objectif de ce sous-projet est de mettre au point une architecture permettant la collaboration d'outils de preuve existants, tant interactifs qu'automatiques. Parmi ces prouveurs, nous pensons notamment à Simplify (Compaq Research), CVC Lite (Stanford University), haRVey (LORIA), Zenon (projet FOCAL), Coq (INRIA), PVS (SRI), Isabelle/HOL (Munich). Par collaboration, nous entendons deux choses : d'une part, l'exécution indépendante de plusieurs prouveurs sur chacune des obligations de preuve, et d'autre part l'utilisation d'un prouveur automatique dans une session de preuve interactive. Nous développerons une architecture qui permettra de sélectionner un sous-ensemble de ces prouveurs à utiliser pour les preuves, ces prouveurs n'étant pas forcément tous disponibles.

Détails des réalisations et échéances

T4.0 Mise en place de l'architecture de collaboration.

Il s'agit de mettre en place une architecture qui permet d'utiliser simultanément plusieurs prouveurs pour établir les obligations de preuve. Cette tâche comporte à la fois une phase de conception pour définir un langage unifié d'expression des obligations et des stratégies de collaboration, puis une phase d'implantation d'un prototype.

T4.1 Intégration dans l'assistant de preuve Coq d'outils de peuve automatiques externes.

Il s'agit de traiter les obligations de preuve qui ne seraient établies par aucun prouveur disponible. Dans ce cas, la preuve demande une intervention de l'utilisateur dans une session de preuve interactive. Dans le cas particulier du prouveur Coq, cette tâche se propose de permettre d'appeler un autre prouveur à l'intérieur même d'une session de preuve interactive. L'utilisateur peut ainsi décomposer le problème de départ en sous-problèmes dont on peut alors espérer que certains deviennent solubles par les outils automatiques.

T4.2 Évaluation des stratégies de preuves et comparaison avec d'autres prouveurs existants

Il s'agit d'évaluer l'architecture mise en place dans les deux premières sous-tâches.

Critère d'évaluation du résultat et de décision de poursuite du sous-projet

Ce sous-projet sera évalué en fonction du taux d'automatisation des preuves des propriétés issues des exemples industriels issus du sous-projet 1. Le support des prouveurs sera progressivement ajouté et ne présentera pas de risque d'échec. La tâche 1 est plus exploratoire mais n'est pas critique pour le projet.

Tâche

Resp.

Début

Fin

Charge (homme/mois)

Délivrables

CEA

INRIA

IRISA

DA

AF

SVDO

FT

T4.0

INRIA

M1

M6

5

5






Rapport

Prototype

T4.1

INRIA

M6

M30

1

12






Rapport

Prototype

T4.2

CEA

M30

M36

4

3






Rapport