@InProceedings{MTFM2019,
author="Mariano M. Moscato and Laura Titolo and Marco A. Feli{\'u} and C{\'e}sar A. Mu{\~{n}}oz",
editor="Maurice H. ter Beek and Annabelle Mclver and Jos{\'e} N. Oliveira",
title="Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm",
booktitle="Formal Methods -- The Next 30 Years",
year="2019",
month="October",
publisher="Springer International Publishing",
series = "Lecture Notes in Computer Science",      
volume = "1180",
address="Porto, Portugal",
pages="21--37",
isbn="978-3-030-30942-8_3",
doi="10.1007/978-3-030-30942-8_3",
abstract="The problem of determining whether or not a point lies inside a given polygon occurs in many applications. In air traffic management concepts, a correct solution to the point-in-polygon problem is critical to geofencing systems for Unmanned Aerial Vehicles and in weather avoidance applications. Many mathematical methods can be used to solve the point-in-polygon problem. Unfortunately, a straightforward floating-point implementation of these methods can lead to incorrect results due to round-off errors. In particular, these errors may cause the control flow of the program to diverge with respect to the ideal real-number algorithm. This divergence potentially results in an incorrect point-in-polygon determination even when the point is far from the edges of the polygon. This paper presents a provably correct implementation of a point-in-polygon method that is based on the computation of the winding number. This implementation is mechanically generated from a source-to-source transformation of the ideal real-number specification of the algorithm. The correctness of this implementation is formally verified within the Frama-C analyzer, where the proof obligations are discharged using the Prototype Verification System (PVS).",
}