Auto-active Verification of Floating-point Programs via Nonlinear Real Provers

TL;DR

This paper presents an automated verification process for floating-point programs using nonlinear real provers, successfully verifying error bounds and functions like sine and square root in SPARK.

Contribution

It introduces a novel verification pipeline combining symbolic simplification, interval arithmetic, and nonlinear real provers, enabling fully verified floating-point functions in SPARK.

Findings

Verified sine and square root functions in SPARK

Achieved tight error bounds for numerical programs

Integrated multiple tools into a cohesive verification process

Abstract

We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions. The process integrates existing tools using a series of transformations and derivations, building on the proving process in SPARK where Why3 produces Verification Conditions (VCs) and tools such as SMT solvers attempt to verify them. We add steps aimed specifically at VCs that contain inequalities with both floating-point operations and exact real functions. PropaFP is our open-source implementation of these steps. The steps include symbolic simplifications, deriving bounds via interval arithmetic, and safely replacing floating-point operations with exact operations, utilizing tools such as FPTaylor or Gappa to bound the compound rounding errors of expressions. Finally, the VCs are passed to provers such as dReal, MetiTarski or LPPaver which attempt to complete the proof or suggest possible counter-examples.