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).
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.
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.
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)
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.
AdaCore has launched the "Make with Ada" competition just today: teams of up to four have until September 30th to submit projects in Ada or SPARK which will be evaluated by a jury of four personalities of the embedded software domain: Bill Wong, Jack Ganssle, Dick Selwood and Cyrille Comar. The 5 prices range from a Crazyflie nano-copter to 5000 euros.
RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write abstract software specifications, whose refinement in terms of concrete implementation can be proved automatically using SPARK tools.
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.
The international team developing the SPARK product, usually dispersed across continents and islands (if UK still counts as an Island despite the Channel Tunnel), has gathered the last week of June to discuss the progress towards SPARK Pro 16.0, and beyond that. Here are the main points that we discussed.
After following for two years the very interesting French conference "Forum Méthodes Formelles", I am now part of the program committee, so will report on interesting topics to SPARK users. The next one is on test and formal methods.