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

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.