The schedule for the Ada Developers’ Room at FOSDEM has been published on the FOSDEM website. There will talks about programming drones in SPARK, parallel computing (in Ada of course), controlling a train model from a Raspberry Pi, etc.
A SPARK package implementing a red-black tree is now available and correctness proofs have been completed for the code. (SPARK correctness is, of course, partial correctness as there are no proofs of termination of the operations.)
In this version the Ada code is complete and all the mandatory SPARK annotations for information flow analysis are included, but the optional proof annotations within the operations in the package body have been excluded. (I have completed these, but they are not yet in a publishable form.)
If you’re in the game of producing secure and high integrity software, SPARK just might be what you’re looking for, and with the newly released SPARK GPL 2011 Edition it’s simple to try your hands at SPARK.
At the libre.adacore.com website, there’s a few community created SPARK projects available. These might be worth checking out for some examples on how to use SPARK. Another option is the AdaCore05 YouTube channel, where there are quite a few SPARK related videos to enjoy.
SPARK is developed by altran praxis.
Yes, I’m that easy to please. :o)
It’s a fairly busy channel, with regular updates. Some of the subjects dealt with are:
And of course lots more. Be sure to check it out!
SPARKRules is a utility program for managing proof libraries – which can contain user rule files and proof review files. SPARKRules allows user rules to be defined once and copied to Simplifier user rule files as required and supports the storage of proof review files in a separate library. The directories generated by the Examiner for the Simplifier are therefore not required for the storage of any permanent data.
You can read the full release announcement here.