Voir la notice de l'article provenant de la source Numdam
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.
Keywords: 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://geodesic.mathdoc.fr/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://geodesic.mathdoc.fr/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://geodesic.mathdoc.fr/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
Cité par Sources :