Langley Formal Methods Program • PolyCARP

PolyCARP (Algorithms and Software for Computations with Polygons) is a package of algorithms, including both their formal models and software implementations, for computing containment, collision, resolution, and recovery information for polygons. The intended applications of PolyCARP are related, but not limited, to safety critical systems in air traffic management.

PolyCARP, including its formalization in PVS, is available under NASA's Open Source Agreement from GitHub.

Publications

• Mariano Moscato, Laura Titolo, Marco Feliú, and César Muñoz, Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm, Proceedings of the 3rd World Congress on Formal Methods (FM 2019), Lecture Notes in Computer Science, Vol. 11800, pp. 21-37, 2019. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, and Aaron Dutle, The MINERVA Software Development Process, Automated Formal Methods, 2017.
• Anthony Narkawicz and George Hagen, Algorithms for Collision Detection Between a Point and a Moving Polygon, With Applications to Aircraft Weather Avoidance, AIAA Aviation 2016, June 13-17, 2016, Washington, D.C.

The tag identifies links that are outside the NASA domain