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.
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)
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.
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.
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.
It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of SPARK Pro, make sure you try it out!
The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My modest Xmas present.
The first module of the free SPARK course on AdaCore U e-learning website (out of five modules) is now available in Japanese, courtesy of Mr. Masao Ito.
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.
We report on the creation of the first lemma of a new lemma library on arrays: a lemma on transitivity of the order in arrays.