Preuves formelles pour le calcul d'enveloppes convexes dans le plan avec des hypercartes
Langue Français
Accéder à la thèse :

Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

 
Auteur : Brun, Christophe
Date de soutenance : 06-12-2010

Directeur(s) de thèse : Dufourd, Jean-François - Magaud, Nicolas


Établissement de soutenance : Université de Strasbourg
École doctorale : École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....)
 
Discipline : Informatique
Classification : Mathématiques

Mots-clés libres : spécification , preuve formelle , hypercarte , carte combinatoire orientée , coq , enveloppe convexe
Mots-clés :
  • Géométrie algorithmique - Thèses et écrits académiques
  • Enveloppes (géométrie) - Thèses et écrits académiques
  • Théorie de la démonstration - Thèses et écrits académiques
  • Programmation fonctionnelle (informatique) - Thèses et écrits académiques
  • Objective Caml (langage de programmation) - Thèses et écrits académiques
Résumé : Notre objectif est de mener une étude formelle dans le domaine de la modélisation géométrique et de la géométrie algorithmique dans le plan afin d'améliorer les techniques de programmation et d'assurer la correction des algorithmes. Nous nous appuyons, d'une part sur les méthodes de spécifications et de preuves formelles du système d'aide à la preuve Coq, et d'autre part sur un cadre de modélisation géométrique à base topologique où les subdivisions du plan sont représentées par des hypercartes. Nous avons mené une étude de cas en géométrie algorithmique sur un problème classique mettant enjeu des subdivisions de surfaces simples puisque réduites à des lignes polygonales : le calcul incrémentaI de l'enveloppe convexe d'un ensemble fmi de points du plan. Nous avons conçu deux algorithmes fonctionnels en Coq dont nous avons extrait automatiquement un programme en OCaml. Puis, nous avons démontré formellement leur correction par la mise en évidence de leurs propriétés topologiques et géométriques. Finalement, nous avons procédé à la dérivation d'un programme efficace en langage impératif (C+) pour une insertion dans la plate-forme de modélisation géométrique de notre équipe.
 
Type de contenu : Text
 
Entrepôt d'origine : Ressource locale
Identifiant : ecrin-ori-303361
Type de ressource : Thèse