Automatic Numerical Solving for Auto-active Verification of Floating-Point Programs

Abstract

We present a new process for the verification of numerical programs with tight functional specifications that feature exact arithmetic including selected transcendental functions. The process, which simplifies, derives bounds, and safely eliminates floating-point operations from Verification Conditions (VCs) produced by Why3, is capable of automatically verifying such specifications and is implemented in our new open source tool named PropaFP. We evaluate PropaFP alongside the state-of-the-art in formal verification of floating-point programs where we find that the process is able to verify specifications that current tools are unable to verify. We also present novel branch-and-prune contractions based on linearisations of conjunctions that consist of nonlinear real inequalities with differentiable expressions. These linearisations and contractions are implemented in our new open source numerical prover named LPPaver. The contractions we have discovered are used to significantly improve the ‘pruning’ step of our branch-and-prune algorithm. We evaluate LPPaver alongside state-of-the-art automated solvers for problems involving nonlinear real arithmetic. LPPaver performs comparably and, in some cases, better than these solvers. Together, PropaFP and LPPaver yield the first fully automatically verified implementations of the sine and square root functions with tight functional specifications.