Taming Floating-Point Rounding Errors with Proofs

Abstract

Developing floating-point software poses significant challenges due to round-off errors inherent in computer arithmetic. These errors can accumulate over the course of numerical computations, significantly affecting the evaluation of both arithmetic and Boolean expressions. Reasoning about floating-point computations is especially important in safety-critical systems, where discrepancies between ideal real-number calculations and their finite-precision implementations can lead to catastrophic consequences.

This talk provides an overview of the application of theorem proving to the formal verification of NASA’s safety-critical avionics software that relies on finite-precision arithmetic. Key applications include geofencing, detect-and-avoid algorithms, and aircraft positioning systems. In particular, the talk highlights how theorem proving has been effectively integrated with static analysis and global optimization tools to develop new toolchains that improve the reliability of floating-point programs and provide formal guarantees of their correctness.

The talk begins with the formal verification of the ADS-B Compact Position Reporting (CPR) algorithm. The Automatic Dependent Surveillance–Broadcast (ADS-B) protocol [14] is a fundamental component of the next generation of air transportation systems, providing direct exchange of precise aircraft state information. The use of ADS-B has been mandatory since 2020 for most commercial aircraft in the U.S. [4] and Europe [7]. Currently, about 100,000 general aviation aircraft are equipped with ADS-B.¹¹1https://generalaviationnews.com/2020/06/13/ads-b-installations-continue-even-in-midst-of-pandemic/ The CPR algorithm is responsible for encoding and decoding aircraft positions in ADS-B messages. Unfortunately, pilots and manufacturers have reported errors in the positions obtained using the CPR algorithm.

In [6], it was formally proven that the original operational requirements of the CPR algorithm were insufficient to guarantee the intended precision, even when assuming computations are performed with exact arithmetic. Therefore, the ideal real-number implementation of CPR has been formally proven correct under a slightly tightened set of requirements. Nevertheless, even under these more restrictive requirements, a straightforward floating-point implementation of the CPR algorithm may still be unsound and produce incorrect results due to round-off errors.

An alternative implementation of the CPR algorithm is presented in [19]. This version includes simplifications that reduce the numerical complexity of the expressions compared to the original version. The double-precision floating-point implementation of this improved version is proven correct using a combination of formal methods tools: the static analyzer Frama-C [8], the interactive theorem prover PVS [13], and Gappa [5], a tool for formally verifying properties of numerical programs.

While successful, the proposed verification approach is not fully automatic and it requires a certain level of expertise. A background in floating-point arithmetic and a deep understanding of the features of each tool is essential for completing the verification. In order to automatize this approach, the PRECiSA static analyzer and the ReFlow code extractor were developed.

PRECiSA[9, 16, 17] is a static analyzer for floating-point programs. It bounds the round-off errors that may occur and produces externally checkable certificates. PRECiSA uses static analysis by abstract interpretation to approximate the collecting semantics of the program and compute symbolic round-off error expressions that model the error along each program trace. The global optimizer Kodiak [15] is used to evaluate these symbolic expressions, producing sound numerical enclosures. PRECiSA generates proof certificates that ensure the correctness of both the symbolic and numerical round-off error estimations. It relies on the higher-order logic interactive theorem prover PVS [13], the floating-point formalization originally presented in [3] and extended in [9], as well as the formalization of Kodiak’s branch-and-bound algorithm [12].

ReFlow [18] is a C code extractor that produces a formally verified floating-point C implementation from a PVS real-number specification. It instruments the code to emit a warning when the floating-point control flow may diverge from the real-number specification due to unstable conditionals, and it automatically generates ACSL [1] annotations that express the relationship between the floating-point implementation and its real-number counterpart.

ReFlow is integrated with the Frama-C analyzer and the PVS theorem prover to provide a fully automatic toolchain for generating and verifying floating-point C code from a PVS real-number specification. In particular, the code generated by ReFlow is used as input to Frama-C, which produces a set of verification conditions in the PVS specification language. Although PVS is an interactive theorem prover, these verification conditions are automatically discharged by ad hoc strategies. As a result, users do not need expertise in theorem proving or floating-point arithmetic to verify the correctness of the generated C program. This verification toolchain has been used to generate C implementations from two formal developments by NASA: the winding number point-in-polygon algorithm used for geofencing applications [10], and a fragment of the DAIDALUS [11] software library [2].

The talk concludes by outlining future challenges in verifying floating-point code, focusing on LLM-generated code and quantized neural networks, which are especially vulnerable to rounding errors.