SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

AdaCore Tech Days Prez on SPARK

by Yannick Moy in Events, Videos – February 19, 2016

Hristian Kirtchev, who leads the developments of the GNAT compiler frontend, gave a very clear presentation of SPARK at the last AdaCore Tech Days in Boston. This was recorded, here is the video.

Christmas Elf Learns SPARK to Automate Toy Delivery by Drone

by Yannick Moy in News – December 14, 2015

To participate in the worldwide effort against global warming, Santa Claus has decided this year to retire his sleight pulled by 1024 reindeers (whose gas emitted at high altitude was threatening to put a premature end to winter season). I have been training some his Christmas elfs to build safe drones which will enter chimneys all over the world to deliver toys to kids. At least some of it is true...

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

by Yannick Moy in Formal Verification – November 30, 2015

SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.

SPARK 2014 Rationale: Support for Ravenscar

by Yannick Moy in Language, Formal Verification – November 23, 2015

As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in the Ravenscar profile of Ada. This profile restricts concurrency so that concurrent programs are deterministic and schedulable. SPARK analysis makes it possible to prove that shared data is protected against data races, that deadlocks cannot occur and that no other run-time errors related to concurrency can be encountered when running the program. In this post, I revisit the example given by Pavlos to show SPARK features and GNATprove analysis in action.

SPARK 2016 supports Ravenscar!

by in Language, Formal Verification – November 12, 2015

The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write concurrent code. On uniprocessor computers the toolset can ensure that no deadlocks or data races will occur and that no tasks will terminate. Read this blog post to learn more and see the new feature in practice.

SPARK 16: Generating Counterexamples for Failed Proofs

by in Formal Verification – November 3, 2015

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.

GNATprove Tips and Tricks: User Profiles

by Yannick Moy in Formal Verification – October 20, 2015

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.