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 metadatas

Cited literature [12 references]  Display  Hide  Download
Contributor : Sylvain Pion <>
Submitted on : Thursday, December 4, 2008 - 4:00:15 PM
Last modification on : Thursday, February 7, 2019 - 5:24:18 PM
Long-term archiving on : Monday, June 7, 2010 - 11:45:11 PM


Files produced by the author(s)




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⟩



Record views


Files downloads