Formal verification of floating-point computations remains a challenge for the software engineer. Automated, specialized tools can handle floating-point computations well, but struggle with other types of data or memory reasoning. In this article, we show how generic deductive verification tools based on general-purpose SMT solvers can be used to verify different kinds of properties on floating point computations up to bounds on rounding er- rors. The demonstration is done on a computation of a weighted average using floating-point numbers, using an approach which is heavily based on auto-active verification. We use the general-purpose tool SPARK for formal verification of Ada programs based on the SMT solvers Alt-Ergo, CVC4, and Z3 but it can in principle be carried out in other similar languages and tools such as Frama-C or KeY.
Making Proofs of Floating-Point Programs Accessible to Regular Developers
