SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Hash it and Cache it

by Johannes Kanig in Formal Verification – January 24, 2017

A new feature of SPARK2014 allows to use a memcached server to share proof results between runs of the SPARK tools and even between developers on different machines. Check out this post to see the details.

Webcast on SPARK Hosted by Electronic Design

by Yannick Moy in Events – December 6, 2016

Next Monday, Bill Wong from Electronic Design will host a free webcast on "Building High-Assurance Software without Breaking the Bank", with SPARK experts Rod Chapman and myself as presenters. You can already register for the event.

Automatic Generation of Frame Conditions for Array Components

by Claire Dross in Formal Verification – November 21, 2016

One of the most important challenges for SPARK users is to come up with adequate contracts and annotations, allowing GNATprove to verify the expected properties in a modular way. Among the annotations mandated by the SPARK toolset, the hardest to come up with are probably loop invariants. A previous post explains how GNATprove can automatically infer loop invariants for preservation of unmodified record components, and so, even if the record is itself nested inside a record or an array. Recently, this generation was improved to also support the simplest cases of partial array updates. We describe in this post in which cases GNATprove can, or cannot, infer loop invariants for preservation of unmodified array components.

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.