Independent SPARK Support

This is the SparkSure homepage

SparkSure is an independent consultancy offering services in the production of high-integrity Ada.

See About Us for who we are and Our Services for details of what we offer.

Contact details are here.

Proof Tutorials

There are two tutorials for using the proof features of SPARK:

one for the optional proof annotations (for proof of absence of run-time error)
and one for the SPADE Proof Checker.

Details of these are on the SPARK Proof Tutorials page.

Proof Tools

We also have a number of tools that help with using the proof features of the SPARK Toolset.

Details of these are on the SPARK Proof Tools page.

High Integrity Data Structures

SPARK has the potential for creating high integrity data structures and the current information on what we have developed is on the Data Structures page.

This now includes the initial release of the red-black tree code, along with the key rules for proving correctness of the code that modifies the tree structure.

Tokeneer Update

The Tokeneer code is an excellent example of SPARK, but the work was completed several years ago and prior to major improvements being made to the proof capabilities of the SPARK Toolset.

I have updated the proofs to make them a better example of how to use user rules and other proof features of the SPARK toolset.

The updated files for the Tokeener reproof including a note describing the changes made and a readme for the updated files are on the Download page.