SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

GNATprove Tips and Tricks: What’s Provable for Real Now?

by Yannick Moy in Formal Verification – November 17, 2016

One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.