by Yannick Moy in Events, News – May 12, 2017
The annual competition "Make with Ada" is starting now. Participants have until Septembre 15th to create an embedded application in Ada or SPARK, using the tools and support we'll put in place for this event. The prizes range from 5000 euros (5500 dollars) to 1000 euros (1100 dollars).
by Yannick Moy in Formal Verification, Events – April 28, 2017
This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure. In this post, I am using this challenge to show how one can reach different levels of software assurance with SPARK.
by Yannick Moy in Events – April 11, 2017
This year, SPARK crowd joins the Frama-C crowd, thus the Frama-C Day around static analysis and formal verification of C programs becomes the Frama-C & SPARK Day. This event takes place in Paris on May 30th, and the program is now available online.
by Yannick Moy in Formal Verification – April 6, 2017
Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first algorithms that humans devised. So it's quite appealing to try to prove it with an automatic proving toolset like SPARK. It turns out that proving it automatically is not so easy, just like understanding why it works is not so easy. In this post, I am using ghost code to prove correct implementations of the GCD, starting from a naive linear search algorithm and ending with Euclid's algorithm.
by Yannick Moy in Dev Projects, Open Source – March 30, 2017
Two projects by Daniel King and Martin Becker facilitate the analysis of GNATprove results by exporting the results (either from the log or from the generated JSON files) to either Excel or JSON/text.
by Claire Dross in Formal Verification, Papers and Slides – March 9, 2017
GNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In SPARK, annotations are most often given in the form of contracts (pre and postconditions). But some language features, in particular ghost code, allow proof guidance to be much more involved. In a paper we are presenting at NASA Formal Methods symposium 2017, we describe how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification.
by Yannick Moy in Events, Videos – March 7, 2017
Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how difficult it is to produce secure software. Of course, it would not be Rod Chapman if he did not have also a few hints at how they have done it at Altran UK over the years. And SPARK is central to this solution, although it does not get mentioned explicitly in the talk! (although Rod lifts the cover in answering a question at the end)
by Yannick Moy in News, Papers and Slides – February 21, 2017
The core part of the SPARK User's Guide, including the fundamental concepts of the SPARK language and the essential features of the SPARK toolset, is now available in Japanese.
by Yannick Moy in Videos – February 10, 2017
I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the recording.
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.