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

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/inria-00344518
Contributor : Sylvain Pion <>
Submitted on : Friday, December 5, 2008 - 3:11:31 AM
Last modification on : Wednesday, November 20, 2019 - 3:27:37 AM
Long-term archiving on: Monday, June 7, 2010 - 9:07:38 PM

File

IMACS_05_FPgeo.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00344518⟩

Share

Metrics

Record views

504

Files downloads

210