×

Formally certified floating-point filters for homogeneous geometric predicates. (English) Zbl 1133.65010

Summary: 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 avoids 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.

MSC:

65D18 Numerical aspects of computer graphics, image analysis, and computational geometry
65G20 Algorithms with automatic result verification
PDFBibTeX XMLCite
Full Text: DOI Numdam EuDML

References:

[1] H. Brönnimann , C. Burnikel and S. Pion , Interval arithmetic yields efficient dynamic filters for computational geometry . Discrete Appl. Math. 109 ( 2001 ) 25 - 47 . Zbl 0967.68157 · Zbl 0967.68157 · doi:10.1016/S0166-218X(00)00231-6
[2] C. Burnikel , S. Funke and M. Seel , Exact geometric computation using cascading . Internat. J. Comput. Geom. Appl. 11 ( 2001 ) 245 - 266 . Zbl 1074.65509 · Zbl 1074.65509 · doi:10.1142/S0218195901000493
[3] The CGAL Manual, 2004. Release 3.1.
[4] 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 ).
[5] O. Devillers and S. Pion , Efficient exact geometric predicates for Delaunay triangulations , in Proc. 5th Workshop Algorithm Eng. Exper. ( 2003 ) 37 - 44 .
[6] S. Fortune and C.J. Van Wyk , Static analysis yields efficient exact integer arithmetic for computational geometry . ACM Trans. Graph. 15 ( 1996 ) 223 - 248 . · Zbl 0873.68197
[7] S. Fortune and C.V. Wyk , LN User Manual . AT&T Bell Laboratories ( 1993 ).
[8] 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 . Zbl 1111.68725 · Zbl 1111.68725 · doi:10.1007/b100428
[9] 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 . · Zbl 1323.68540
[10] A. Neumaier , Interval methods for systems of equations . Cambridge University Press ( 1990 ). MR 1100928 | Zbl 0715.65030 · Zbl 0715.65030 · doi:10.1017/CBO9780511526473
[11] 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.
[12] J.R. Shewchuk , Adaptive precision floating-point arithmetic and fast robust geometric predicates . Discrete Comput. Geom. 18 ( 1997 ) 305 - 363 . Zbl 0892.68098 · Zbl 0892.68098 · doi:10.1007/PL00009321
[13] D. Stevenson et al., An American national standard: IEEE standard for binary floating point arithmetic . ACM SIGPLAN Notices 22 ( 1987 ) 9 - 25 .
[14] 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 .
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.