# Formally certified floating-point filters for homogeneous geometric predicates

Guillaume Melquiond; Sylvain Pion

RAIRO - Theoretical Informatics and Applications (2007)

- Volume: 41, Issue: 1, page 57-69
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topMelquiond, Guillaume, and Pion, Sylvain. "Formally certified floating-point filters for homogeneous geometric predicates." RAIRO - Theoretical Informatics and Applications 41.1 (2007): 57-69. <http://eudml.org/doc/250074>.

@article{Melquiond2007,

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.
},

author = {Melquiond, Guillaume, Pion, Sylvain},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Geometric predicates; semi-static filters; formal proofs;
floating-point; floating-point arithmetic; verification},

language = {eng},

month = {4},

number = {1},

pages = {57-69},

publisher = {EDP Sciences},

title = {Formally certified floating-point filters for homogeneous geometric predicates},

url = {http://eudml.org/doc/250074},

volume = {41},

year = {2007},

}

TY - JOUR

AU - Melquiond, Guillaume

AU - Pion, Sylvain

TI - Formally certified floating-point filters for homogeneous geometric predicates

JO - RAIRO - Theoretical Informatics and Applications

DA - 2007/4//

PB - EDP Sciences

VL - 41

IS - 1

SP - 57

EP - 69

AB -
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.

LA - eng

KW - Geometric predicates; semi-static filters; formal proofs;
floating-point; floating-point arithmetic; verification

UR - http://eudml.org/doc/250074

ER -

## References

top- H. Brönnimann, C. Burnikel and S. Pion, Interval arithmetic yields efficient dynamic filters for computational geometry. Discrete Appl. Math.109 (2001) 25–47.
- C. Burnikel, S. Funke and M. Seel, Exact geometric computation using cascading. Internat. J. Comput. Geom. Appl.11 (2001) 245–266.
- The CGAL Manual, 2004. Release 3.1.
- M. Daumas and G. Melquiond, Generating formally certified bounds on values and round-off errors, in 6th Conference on Real Numbers and Computers. Dagstuhl, Germany (2004).
- O. Devillers and S. Pion, Efficient exact geometric predicates for Delaunay triangulations, in Proc. 5th Workshop Algorithm Eng. Exper. (2003) 37–44.
- S. Fortune and C.J. Van Wyk, Static analysis yields efficient exact integer arithmetic for computational geometry. ACM Trans. Graph.15 (1996) 223–248.
- S. Fortune and C.V. Wyk, LN User Manual. AT&T Bell Laboratories (1993).
- L. Kettner, K. Mehlhorn, S. Pion, S. Schirra and C. Yap, Classroom examples of robustness problems in geometric computations, in Proc. 12th European Symposium on Algorithms, Lect. Notes Comput. Sci.3221 (2004) 702–713.
- A. Nanevski, G. Blelloch and R. Harper, Automatic generation of staged geometric predicates, in International Conference on Functional Programming, Florence, Italy (2001). Also Carnegie Mellon CS Tech Report CMU-CS-01-141.
- A. Neumaier, Interval methods for systems of equations. Cambridge University Press (1990).
- S. Pion, De la géométrie algorithmique au calcul géométrique. Thèse de doctorat en sciences, Université de Nice-Sophia Antipolis, France (1999). TU-0619.
- J.R. Shewchuk, Adaptive precision floating-point arithmetic and fast robust geometric predicates. Discrete Comput. Geom.18 (1997) 305–363.
- D. Stevensonet al., An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices22 (1987) 9–25.
- C.K. Yap, T. Dubé, The exact computation paradigm, in Computing in Euclidean Geometry, edited by D.-Z. Du and F.K. Hwang, World Scientific, Singapore, 2nd edition, Lect. Notes Ser. Comput.4 (1995) 452–492.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.