Independent SPARK Support

Proof Tutorials

Download the Proof of Absence of Run-Time Error tutorial (442 kB).

Download the SPADE Proof Checker tutorial (333 kB).

Proof Tools

The executables are for Windows only.  The programs are Ada, compiled using GPS 4.2.1 and
GNAT GPL 2008, so could be compiled for other platforms if required.

GtkAda 2.10.2 has been used for the graphical interface for both programs.

The executables with all the required binaries are in this file (6.2 Mb).

The executables without the additional binaries are in this file (641 Kb).

Release 2.02 for PCHIF is in this file (406 Kb).  (It is included in both of the above.)

Tokeener Proof

The updated files, along with a description and a readme are in this file (123 Kb).