An integrated approach to high integrity software verification

Andrew Ireland, Bill J. Ellis, Andrew Cook, Roderick Chapman, Janet Barnes

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

Using automated reasoning techniques, we tackle the niche activity of proving that a program is free from run-time exceptions. Such a property is particularly valuable in high integrity software, for example, safety- or security-critical applications. The context for our work is the SPARK Approach for the development of high integrity software. The SPARK Approach provides a significant degree of automation in proving exception freedom. Where this automation fails, however, the programmer is burdened with the task of interactively constructing a proof and possibly also having to supply auxiliary program annotations. We minimize this burden by increasing the automation, through an integration of proof planning and a program analysis oracle. We advocate a 'cooperative' integration, where proof-failure analysis directly constrains the search for auxiliary program annotations. The approach has been successfully tested on industrial data. © Springer Science+Business Media, Inc. 2007.

Original languageEnglish
Pages (from-to)379-410
Number of pages32
JournalJournal of Automated Reasoning
Volume36
Issue number4
DOIs
Publication statusPublished - Apr 2006

Keywords

  • Program proof
  • Proof planning
  • SPARK
  • Static analysis

Fingerprint Dive into the research topics of 'An integrated approach to high integrity software verification'. Together they form a unique fingerprint.

Cite this