Recherche et téléchargement d’archives de revues mathématiques numérisées

  Table des matières de ce fascicule | Article précédent | Article suivant
Melquiond, Guillaume; Pion, Sylvain
Formally certified floating-point filters for homogeneous geometric predicates. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 41 no. 1 (2007), p. 57-69
Texte intégral djvu | pdf | Analyses MR 2330043 | Zbl 1133.65010
Class. Math.: 65D18, 65G50, 68Q60
Mots clés: geometric predicates, semi-static filters, formal proofs, floating-point

URL stable:

Voir cet article sur le site de l'éditeur


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.


[1] H. Brönnimann, C. Burnikel and S. Pion, Interval arithmetic yields efficient dynamic filters for computational geometry. Discrete Appl. Math. 109 (2001) 2547.  Zbl 0967.68157
[2] C. Burnikel, S. Funke and M. Seel, Exact geometric computation using cascading. Internat. J. Comput. Geom. Appl. 11 (2001) 245266.  Zbl 1074.65509
[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) 3744.
[6] S. Fortune and C.J. Van Wyk, Static analysis yields efficient exact integer arithmetic for computational geometry. ACM Trans. Graph. 15 (1996) 223248.
[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) 702713.  Zbl 1111.68725
[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.
[10] A. Neumaier, Interval methods for systems of equations. Cambridge University Press (1990).  MR 1100928 |  Zbl 0715.65030
[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) 305363.  Zbl 0892.68098
[13] D. Stevenson et al., An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices 22 (1987) 925.
[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) 452492.
Copyright Cellule MathDoc 2016 | Crédit | Plan du site