For the first time this year, we're issuing release notes for SPARK Pro in HTML, with code snippets and links to relevant external information.
SPARK Discovery GPL 2017 is out! With more automation of proofs, new modes of user interaction, support for type invariants. Note that the optional provers CVC4 and Z3 are no longer distributed with SPARK Discovery GPL 2017, and should be installed separately.
The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with Frama-C) and for Ada programs (with SPARK). Here is a summary of what was interesting for SPARK users. We also point to the slides of the presentations.
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).
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.
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.
Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar IceCube that will map water vapor and ice on the moon. In their paper, they explain how the use of proof with SPARK is going to help them get perfect software in the time and budget available.
The repository on the open-do forge is now obsolete. SPARK2014 and its components Why3, Alt-Ergo, CVC4 and Z3 are available on github.
The annual releases of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from libre.adacore.com. For SPARK, this means support of concurrency with Ravenscar, generation of counterexamples and better proof automation. Enjoy!
The new version 16 of SPARK Pro toolset is now available for AdaCore's customers. See demo online.