kirancodes.me
To Proof Maintenance & Beyond!
ASE 2003

Automation for Exception Freedom Proofs

Bill J. Ellis, Andrew Ireland

DOI 10.1109/ase.2003.1240334dblp

Abstract

Run-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.

BibTeX
@inproceedings{Ellis-Ireland:ASE03,
  author    = {Bill J. Ellis and
               Andrew Ireland},
  title     = {Automation for Exception Freedom Proofs},
  booktitle = {ASE},
  pages     = {343--346},
  publisher = {{IEEE} Computer Society},
  year      = {2003},
}

Related papers