Tommy Ingulfsen [ Dissertation Project Student, 2002-2003 ]
Andrew Cook [ Programmer, Spring 2004 ]
Overview
An investigation into the role that
Proof Planning can play
within the formal verification of software written in
SPARK. SPARK is
a subset of the Ada programming language developed by
Praxis High Integrity Systems Ltd
(previously known as Praxis Critical Systems Ltd).
This involved adding a proof planning capability to the
SPADE Proof Checker - an interactive proof tool that is
used to discharge verification conditions associated with
SPARK code. The resulting system, which is called NuSPADE,
provides a tight integration between proof planning and program analysis.
In particular, we use proof-failure analysis to selectively strengthen
SPARK specifications. We believe
that NuSPADE has significantly reduced the amount and sophistication
of interactions currently required by SPADE users.
The original proposal can be accessed in either
pdf or
postscript formats. This 3-year project was in collaboration with
Praxis High Integrity Systems and is funded under the EPSRC Critical Systems
Programme (EPSRC grant GR/R24081: 01/09/2001 - 31/08/2004).
An overview of the NuSPADE project appeared in the
ERCIM News.
The final report (pdf) for the project can be accessed
here. Details of a follow-on ``knowledge transfer'' project funded
by the EPSRC RAIS Scheme can be access
here.
Further details can be obtained from Andrew Ireland,
Dependable Systems Group,
School of Mathematical and Computer Sciences,
Heriot-Watt University, Edinburgh, EH14 4AS, UK
[ a.ireland@hw.ac.uk, +44 (0)131 451 3409 ]