Automatic generation and verification of test-stable floating-point code

TL;DR

This paper introduces a toolchain that automatically generates and verifies floating-point programs to ensure test stability, preventing divergence caused by round-off errors in safety-critical numerical applications.

Contribution

It presents a novel integrated approach combining PVS, Frama-C, and PRECiSA to automatically produce and verify test-stable floating-point code from real arithmetic specifications.

Findings

Successfully detects potential test instability in floating-point programs.

Automatically generates C code with ACSL contracts linked to real arithmetic.

Verifies correctness of floating-point code ensuring it follows the real-valued specification.

Abstract

Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by the presence of round-off errors that affect the evaluation of arithmetic expressions occurring in conditional statements. Unstable tests may lead to significant errors in safety-critical applications that depend on numerical computations. Writing programs that take into consideration test instability is a difficult task that requires expertise on finite precision computations and rounding errors. This paper presents a toolchain to automatically generate and verify a provably correct test-stable floating-point program from a functional specification in real arithmetic. The input is a real-valued program written in the Prototype Verification System (PVS) specification language and the output is a transformed floating-point C program annotated with ANSI/ISO C Specification Language (ACSL) contracts. These contracts relate the floating-point program to its functional specification in real arithmetic. The transformed program detects if unstable tests may occur and, in these cases, issues a warning and terminate. An approach that combines the Frama-C analyzer, the PRECiSA round-off error estimator, and PVS is proposed to automatically verify that the generated program code is correct in the sense that, if the program terminates without a warning, it follows the same computational path as its real-valued functional specification.