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

Technical Report HW-MACS-TR-0010

TitleAutomation for Exception Freedom Proofs
AuthorsBill J. Ellis, Andrew Ireland
AbstractRun-time errors are typically seen as unacceptable within safety and security critical software. The SPARK approach to the development of high integrity software addresses the problem of run-time errors through the use of formal verification. Proofs are constructed to show that each run-time check will never raise an error, thus proving freedom from run-time exceptions. Here we build upon the success of the SPARK approach by increasing the level of automation that can be achieved in proving freedom from exceptions. Our approach is based upon proof planning and a form of abstract interpretation.


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