@inbook{25c1d9e7d5574aae82b0bcb08a47ff08,
title = "An integration of program analysis and automated theorem proving",
abstract = "Finding tractable methods for program reasoning remains a major research challenge. Here we address this challenge using an integrated approach to tackle a niche program reasoning application. The application is proving exception freedom, i.e. proving that a program is free from run-time exceptions. Exception freedom proofs are a significant task in the development of high integrity software, such as safety and security critical applications. The SPARK approach for the development of high integrity software provides a significant degree of automation in proving exception freedom. However, when the automation fails, user interaction is required. We build upon the SPARK approach to increase the amount of automation available. Our approach involves the integration of two static analysis techniques. We extend the proof planning paradigm with program analysis. {\textcopyright} Springer-Verlag 2004.",
author = "Ellis, {Bill J.} and Andrew Ireland",
year = "2004",
doi = "10.1007/978-3-540-24756-2_5",
language = "English",
isbn = "978-3-540-21377-2",
volume = "2999",
series = "Lecture Notes in Computer Science",
pages = "67--86",
booktitle = "Integrated Formal Methods",
note = "4th International Conference on Integrated Formal Methods, IFM 2004 ; Conference date: 04-04-2004 Through 07-04-2004",
}