HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071232
Contributor : Sylvain Pion Connect in order to contact the contributor
Submitted on : Thursday, December 4, 2008 - 4:00:15 PM
Last modification on : Friday, February 4, 2022 - 3:22:41 AM
Long-term archiving on: : Monday, June 7, 2010 - 11:45:11 PM

File

pion_melquiond.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

294

Files downloads

567