An integration of program analysis and automated theorem proving

Bill J. Ellis, Andrew Ireland

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

6 Citations (Scopus)

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. © Springer-Verlag 2004.

Original languageEnglish
Title of host publicationIntegrated Formal Methods
Subtitle of host publication4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004. Proceedings
Pages67-86
Number of pages20
Volume2999
ISBN (Electronic)978-3-540-24756-2
DOIs
Publication statusPublished - 2004
Event4th International Conference on Integrated Formal Methods - Canterbury, United Kingdom
Duration: 4 Apr 20047 Apr 2004

Publication series

NameLecture Notes in Computer Science
Volume2999
ISSN (Print)0302-9743

Conference

Conference4th International Conference on Integrated Formal Methods
Abbreviated titleIFM 2004
Country/TerritoryUnited Kingdom
CityCanterbury
Period4/04/047/04/04

Fingerprint

Dive into the research topics of 'An integration of program analysis and automated theorem proving'. Together they form a unique fingerprint.

Cite this