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.
AdaCore University is hosting a 5-lessons course on SPARK 2014, which gives a complete overview of the technology.
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...
I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!
A new course on university.adacore.com presents the SPARK language and tools. The first lecture is now online, and others will follow this year.