An Integrated Approach to High Integrity Software Verification

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, e.g. 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. However, where this automation fails, the programmer is burdened with the task of interactively constructing a proof and possibly also having to supply auxiliary program annotations. We minimise this burden by increasing the automation, via an integration of proof planning and a program analysis oracle. We advocate a "co-operative" integration, where proof-failure analysis directly constrains the search for auxiliary program annotations. The approach has been successfully tested on industrial data.

• Type: Journal
• Year: 2006
• Where: JAR
• Authors: Andrew Ireland, Bill J. Ellis, Andrew Cook, Roderick Chapman, Janet Barnes
• Keywords: Auxiliary Program Annotations, JAR 2006, Security Critical Applications, SPARK Approach