Formal certification of arithmetic filters for geometric predicates

Abstract : Floating-point arithmetic provides a fast but inexact way of computing geometric predicates. In order for these predicates to be exact, it is important to rule out all the numerical situations where floating-point computations could lead to wrong results. Taking into account all the potential problems is a tedious work to do by hand. We study in this paper a floating-point implementation of a filter for the orientation-2 predicate, and how a formal and partially automatized verification of this algorithm avoided many pitfalls. The presented method is not limited to this particular predicate, it can easily be used to produce correct semi-static floating-point filters for other geometric predicates.
Type de document :
Communication dans un congrès
17th IMACS World Congress, 2005, Paris, France. 2005
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00344518
Contributeur : Sylvain Pion <>
Soumis le : vendredi 5 décembre 2008 - 03:11:31
Dernière modification le : vendredi 20 avril 2018 - 15:44:24
Document(s) archivé(s) le : lundi 7 juin 2010 - 21:07:38

Fichier

IMACS_05_FPgeo.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00344518, version 1

Collections

Citation

Guillaume Melquiond, Sylvain Pion. Formal certification of arithmetic filters for geometric predicates. 17th IMACS World Congress, 2005, Paris, France. 2005. 〈inria-00344518〉

Partager

Métriques

Consultations de la notice

400

Téléchargements de fichiers

165