Technical Report HW-MACS-TR-0027
|Title||An Integrated Approach to High Integrity Software Verification|
|Authors||Andrew Ireland, Bill Ellis, Andrew Cook, Roderick Chapman, Janet Barnes|
|Abstract||Using automated reasoning techniques, we tackle the niche activity of proving that a program is free from run-time exceptions. Such a property is particularly valuable in high integrity software, e.g. safety or security critical applications. The context for our work is the SPARK Approach for the development of high integrity software.
The SPARK Approach provides a significant degree of automation in proving exception freedom. However, where this automation fails, the programmer is burdened with the task of interactively constructing a proof and possibly also having to supply auxiliary program annotations. We minimise this burden by increasing the automation, via an integration of proof planning and a program analysis oracle. We advocate a "co-operative" integration, where proof-failure analysis directly constrains the search for auxiliary program annotations. The approach has been successfully tested on industrial data.|