Formally Certified Floating-Point Filters For Homogeneous Geometric Predicates

Guillaume Melquiond 1 Sylvain Pion 2
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
2 GEOMETRICA - Geometric computing
CRISAM - Inria Sophia Antipolis - Méditerranée
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 :
Article dans une revue
RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2007, 41, pp.57-69. 〈10.1051/ita:2007005〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00071232
Contributeur : Sylvain Pion <>
Soumis le : jeudi 4 décembre 2008 - 16:00:15
Dernière modification le : samedi 21 avril 2018 - 01:27:39
Document(s) archivé(s) le : lundi 7 juin 2010 - 23:45:11

Fichier

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

Identifiants

Collections

Citation

Guillaume Melquiond, Sylvain Pion. Formally Certified Floating-Point Filters For Homogeneous Geometric Predicates. RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2007, 41, pp.57-69. 〈10.1051/ita:2007005〉. 〈inria-00071232v2〉

Partager

Métriques

Consultations de la notice

403

Téléchargements de fichiers

323