Tech Reports Home Contact
Technical Report Series
Submit Report
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0027

TitleAn Integrated Approach to High Integrity Software Verification
AuthorsAndrew Ireland, Bill Ellis, Andrew Cook, Roderick Chapman, Janet Barnes
AbstractUsing 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.
GroupDependable Systems


Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer