Collaboration des outils de preuve.
Début : M1
Fin : M36
Responsable : INRIA
Participants : INRIA, CEA
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.
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.
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 |