|
|
|
|
|
|
|
Technical Report HW-MACS-TR-0014
Title | An Integration of Program Analysis and Automated Theorem Proving |
---|
Authors | Bill J. Ellis, Andrew Ireland |
---|
Date | 2004-01-27 |
---|
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. |
---|
Group | DSG |
---|
Notes | |
---|
Download | |
---|
|
|
|
|
|
Email
Technical Report's Administrator |
|
|
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 |
|