CPR*: Formally Verified Compact Position Reporting Algorithm(LAR-19679-1)

The Compact Position Reporting (CPR) algorithm consists of a set of functions defined in the standard RTCA-DO-260B/Eurocae ED-102A, Minimum Operational Performance Standards for 1090 MHz extended squitter Automatic Dependent Surveillance - Broadcast (ADS- B) and Traffic Information Services - Broadcast (TIS-B). These functions encode and decode aircraft positions. CPR* is a formally verified implementation of CPR's functions using computer arithmetic in fixed- and floating-point formats.