SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Research Corner - Floating-Point Computations in SPARK

by Yannick Moy in Formal Verification, Papers and Slides – June 8, 2017

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.