Nous proposonsd'effectuer en CtCoq la preuve formelle d'algorithmes de géométrie. En premier, lieu on s'intéressera à l'algorithme de calcul d'une enveloppe convexe en dimension deux par la méthode du paquet cadeau. Si le temps le permet, ce travail pourra être étendu à des algorithmes plus genéraux, valables également pour des dimensions plus grandes. L'étudiant devra d'une part décrire formellement l'algorithme et d'autre part décrire formellement la notion d'enveloppe convexe pour montrer que le résultat de l'algorithme retourne effectivement une enveloppe convexe.
CtCoq est un environnement de preuve construit autour du système Coq. Cet environnement fournit une interface conviviale pour utiliser des notations adaptées au domaine mathématique envisagé et interagir à la souris avec les formules mathématiques. De plus, les recherches récentes sur ce système visent à faciliter le développement de grandes preuves entièrement formalisées.
Ce travail sur les algorithmes de géométrie permettra à l'étudiant d'approfondir sa connaissance des structures de base de la géométrie, de la programmation et de la logique. Les algorithmes envisagés seront tirés de la littérature et il n'est donc pas nécessaire d'avoir des connaissances très profondes dans ce domaine. En revanche, une bonne connaissance de la logique et de la preuve sur ordinateur est appréciable, car les preuves seront intégralement vérifiées par ordinateur.
En utilisant les capacités d'extraction de Coq, il sera possible des programmes de ces preuves d'algorithmes. L'étudiant aura donc développé un programme certifié en géométrie.
Tel: 04 92 38 77 39
INRIA Sophia Antipolis
[1] J.-D. Boissonnat, M. Yvinec, Géométrie Algorithmique, Ediscience international, Paris, 1995.
[2] R. Sedgewick, Algorithms, Addison-Wesley series in compotuer science, Assison-Wesley, 1988.
[3] B. Barras, S. Boutin, C. Cornes, J. courant, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, B. Werner, "The Coq Proof Assistant Reference Manual Version 6.1", Rapport Technique INRIA 0203, mai 1997.
[4] Yves Bertot, CtCoq on-line help.
Retour aux autres stages proposés dans le projet.