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.
Mots-clés : geometric predicates, semi-static filters, formal proofs, floating-point
@article{ITA_2007__41_1_57_0, author = {Melquiond, Guillaume and Pion, Sylvain}, title = {Formally certified floating-point filters for homogeneous geometric predicates}, journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications}, pages = {57--69}, publisher = {EDP-Sciences}, volume = {41}, number = {1}, year = {2007}, doi = {10.1051/ita:2007005}, mrnumber = {2330043}, zbl = {1133.65010}, language = {en}, url = {http://www.numdam.org/articles/10.1051/ita:2007005/} }
TY - JOUR AU - Melquiond, Guillaume AU - Pion, Sylvain TI - Formally certified floating-point filters for homogeneous geometric predicates JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2007 SP - 57 EP - 69 VL - 41 IS - 1 PB - EDP-Sciences UR - http://www.numdam.org/articles/10.1051/ita:2007005/ DO - 10.1051/ita:2007005 LA - en ID - ITA_2007__41_1_57_0 ER -
%0 Journal Article %A Melquiond, Guillaume %A Pion, Sylvain %T Formally certified floating-point filters for homogeneous geometric predicates %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2007 %P 57-69 %V 41 %N 1 %I EDP-Sciences %U http://www.numdam.org/articles/10.1051/ita:2007005/ %R 10.1051/ita:2007005 %G en %F ITA_2007__41_1_57_0
Melquiond, Guillaume; Pion, Sylvain. Formally certified floating-point filters for homogeneous geometric predicates. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 41 (2007) no. 1, pp. 57-69. doi : 10.1051/ita:2007005. http://www.numdam.org/articles/10.1051/ita:2007005/
[1] Interval arithmetic yields efficient dynamic filters for computational geometry. Discrete Appl. Math. 109 (2001) 25-47. | Zbl
, and ,[2] Exact geometric computation using cascading. Internat. J. Comput. Geom. Appl. 11 (2001) 245-266. | Zbl
, and ,[3] The CGAL Manual, 2004. Release 3.1.
[4] Generating formally certified bounds on values and round-off errors, in 6th Conference on Real Numbers and Computers. Dagstuhl, Germany (2004).
and ,[5] Efficient exact geometric predicates for Delaunay triangulations, in Proc. 5th Workshop Algorithm Eng. Exper. (2003) 37-44.
and ,[6] Static analysis yields efficient exact integer arithmetic for computational geometry. ACM Trans. Graph. 15 (1996) 223-248.
and ,[7] LN User Manual. AT&T Bell Laboratories (1993).
and ,[8] Classroom examples of robustness problems in geometric computations, in Proc. 12th European Symposium on Algorithms, Lect. Notes Comput. Sci. 3221 (2004) 702-713. | Zbl
, , , and ,[9] 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.
, and ,[10] Interval methods for systems of equations. Cambridge University Press (1990). | MR | Zbl
,[11] 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] Adaptive precision floating-point arithmetic and fast robust geometric predicates. Discrete Comput. Geom. 18 (1997) 305-363. | Zbl
,[13] An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices 22 (1987) 9-25.
et al.,[14] 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.
, ,- Verified Numerical Computations for Searching for Vectors with the Maximum Sum, Journal of Advanced Simulation in Science and Engineering, Volume 8 (2021) no. 1, p. 53 | DOI:10.15748/jasse.8.53
- GPredicates: GPU Implementation of Robust and Adaptive Floating-Point Predicates for Computational Geometry, IEEE Access, Volume 7 (2019), p. 60868 | DOI:10.1109/access.2019.2911641
- Extension of floating-point filters to absolute and relative errors for numerical computation, Journal of Physics: Conference Series, Volume 1218 (2019) no. 1, p. 012011 | DOI:10.1088/1742-6596/1218/1/012011
- Bibliography, Floating-Point Algorithms and Formal Proofs (2017), p. 289 | DOI:10.1016/b978-1-78548-112-3.50015-1
- Simple floating-point filters for the two-dimensional orientation problem, BIT, Volume 56 (2016) no. 2, pp. 729-749 | DOI:10.1007/s10543-015-0574-9 | Zbl:1347.65050
- A Configurable, Inexpensive, Portable, Multi-channel, Multi-frequency, Multi-chromatic RGB LED System for SSVEP Stimulation, Brain-Computer Interfaces, Volume 74 (2015), p. 241 | DOI:10.1007/978-3-319-10978-7_9
- Further analysis of Kahan's algorithm for the accurate computation of
determinants, Mathematics of Computation, Volume 82 (2013) no. 284, pp. 2245-2264 | DOI:10.1090/s0025-5718-2013-02679-8 | Zbl:1277.65026 - A robust algorithm for geometric predicate by error-free determinant transformation, Information and Computation, Volume 216 (2012), pp. 3-13 | DOI:10.1016/j.ic.2011.09.007 | Zbl:1257.65010
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa, IEEE Transactions on Computers, Volume 60 (2011) no. 2, p. 242 | DOI:10.1109/tc.2010.128
- Certification of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, Volume 37 (2010) no. 1, p. 1 | DOI:10.1145/1644001.1644003
- Formal Study of Plane Delaunay Triangulation, Interactive Theorem Proving, Volume 6172 (2010), p. 211 | DOI:10.1007/978-3-642-14052-5_16
- Exact Geometric and Algebraic Computations in CGAL, Mathematical Software – ICMS 2010, Volume 6327 (2010), p. 96 | DOI:10.1007/978-3-642-15582-6_20
- Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven, IEEE Transactions on Computers, Volume 58 (2009) no. 2, p. 220 | DOI:10.1109/tc.2008.200
- Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd, IEEE Transactions on Computers, Volume 57 (2008) no. 4, p. 462 | DOI:10.1109/tc.2007.70819
Cité par 14 documents. Sources : Crossref, zbMATH