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.

GtkAda gpl-2.14.1 has been used for the graphical interface for both programs. 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).

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

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

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 (August 2010) is here (462Kb).

Tokeener Proof

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