It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference. In this article, we describe the mechanisms for adapting the formulas to prove to different provers based on  different technologies to interpret floating-point computations. As we already presented on this blog, the improvements in particular with the abstract interpreter CodePeer and the SMT prover Z3 are very important.

One figure from the article which explains well the current situation is the following:

In order to prove the postcondition of the procedure analyzed (last line), it is necessary to insert 12 intermediate assertions in the source code, which are proved each by one of the provers provided with SPARK Pro (CVC4, ALt-Ergo, Z3 and CodePeer). The green cells in that figure correspond to provers which prove the corresponding formula, with the time they take for that in seconds. Some of these assertions require the use of ghost code to define entities only meant for verification.

While this may seem like a lot of work to prove here a single postcondition, you may convince yourself by reading the article (where we give a mathematical argument for the proof) that this is not trivial either. And the improvements we observed with provers not (yet) included in SPARK (the provers AE_fpa and Colibri on the right hand side of the figure) give us much hope that the situation is going to improve a lot in the coming year.