a1 Laboratoire de l'informatique du parallélisme, UMR 5668 CNRS, ENS Lyon, INRIA, UCBL, 46 allée d'Italie, 69364 Lyon Cedex 07, France; Guillaume.Melquiond@ens-lyon.fr
a2 INRIA Sophia-Antipolis, 2004 route des Lucioles, BP 93, 06902 Sophia-Antipolis, France; Sylvain.Pion@sophia.inria.fr
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.
(Online publication April 24 2007)
Mathematics Subject Classification: