Independent SPARK Support

Proof Tutorials

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

Download the SPADE Proof Checker tutorial (906 kB).

Proof Tools

The executables are for Windows only.  The programs are Ada, compiled using GPS 4.4.1 and
GNAT GPL 2010.

SPARKRules Release 1.0 is in this file (607 Kb).  Sources are included and the code works on both Windows and Linux (tested with openSUSE 11.3).

PCHIF Release 2.03 is in this file (1054 Kb).

VC_View Release 2.1.1 is in this file (485 Kb).

GtkAda gpl-2.14.1 has been used for the graphical interface for PCHIF and VC_View. The binaries for GtkAda can be downloaded from http://libre.adacore.com/libre/download/. (But you may already have them - they are included with GPS 4.4.1 for example).

The source distribution for VC_View is here (118 Kb). This code works on Windows and Linux.

POGS Summary Rule List

The Windows executable, with all the modified files is here (389 Kb).

The patch file (created using git for windows - msysgit) is here (214Kb).

High Integrity Data Structures

 The current version of the data structures (September 2010) is here (865Kb).

Tokeener Proof

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