Formalisation d'algorithmes d'enveloppe convexe/
Formalizing convex hull algorithms
Yves Bertot
Projet Lemme -- INRIA Sophia-Antipolis
Collaboration avec David Pichardie de l'ENS Cachan Bretagne
Abstract:
Nous étudions le développement d'algorithmes
géométriques dont la correction est formellement
vérifiée. Le résultat de ce travail est une
description formelle des principes de base qui font marcher ces
algorithmes, et deux programmes qui effectuent ce calcul et ont
été obtenus automatiquement à partir des preuves
formelles. Une attention particulière a été
portée au traitement des cas
dégénérés qui sont souvent ignorés
par les présentation conventionnelle de l'algorithmique
géométrique.
We study the development of formally proved algorithms for
computational geometry. The result of this work is a formal
description of the basic principles that make convex hull algorithms
work and two programs that implement convex hull computation and have
been automatically obtained from formally verified mathematical
proofs. A special attention has been given to handling degenerated
cases that are often overlooked by conventional algorithm
presentations.
Un article présentant ces travaux
est disponible
ici.
Il sera publié dans les actes de la conférence
Theorem Proving in Higher Order Logics (TPHOLS)
Back to schedule.
Marieke Huisman
Last modified: Fri May 4 16:27:16 MET DST 2001