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
topHow 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 ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.