NuSPADE: Automatic Guidance for the Formal Verification of High Integrity Ada

Project Team


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 [, +44 (0)131 451 3409 ]

| Publications | Presentations | Project Pages | SPADEase |