Logo de l'E.N.T. Alsace
Thèses électroniques Service Commun de la documentation
Logo de l'Université de Strasbourg
Thèses et Mémoire de l'Université de Strasbourg

Preuves formelles pour le calcul d’enveloppes convexes dans le plan avec des hypercartes

BRUN, Christophe (2010) Preuves formelles pour le calcul d’enveloppes convexes dans le plan avec des hypercartes. Thèses de doctorat, Université de Strasbourg.

Plein texte disponible en tant que :

PDF - Un observateur de PDF est nécessaire, comme par exemple GSview, Xpdf or Adobe Acrobat Reader
943 Kb

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 d'EPrint:Thèse de doctorat
Discipline de la thèse / mémoire / rapport :Sciences et Technologies. Informatique
Mots-clés libres:spécification ; preuve formelle ; hypercarte ; carte combinatoire orientée ; coq ; enveloppe convexe
Sujets:UNERA Classification UNERA > ACT Domaine d'activité UNERA > ACT-10 Informatique
CL Classification > DDC Dewey Decimal Classification > 500 Sciences de la nature et mathématiques > 510 Mathématiques > 518 Analyse numérique > 518.1 Algorithmes
Classification Thèses Unistra > Sciences, technologies > Sciences de la nature et mathématiques > 510 Mathématiques > 518 Analyse numérique > 518.1 Algorithmes

UNERA Classification UNERA > DISC Discipline UNERA > DISC-19 Mathématiques et informatique
Code ID:1977
Déposé le :27 Janvier 2011

Administrateurs de l'archive uniquement : éditer cet enregistrement