SPARK in Refereed Journals

Where indicated, PDF downloads of these publications are available for download here. Where PDF is not available, please contact us for how to obtain hardcopies.

"Panellist position statement: some industrial experience with program verification"
Roderick Chapman, Praxis High Integrity Systems
Philosophical Transactions of the Royal Society, October 2005
Abstract
As the only obvious ‘industrial’ member of the panel, I would like to introduce myself and the work I am involved with. Praxis is a practising software engineering company that is well known for applying so-called ‘Formal Methods’ in the development of high-integrity software system. We are also responsible for the SPARK programming language and verification tools (John Barnes with Praxis High Integrity Systems 2003). SPARK remains one of the very few technologies to offer a sound verification system for an industrially usable imperative programming language. Despite the popular belief that ‘no one does formal methods’, we (and our customers) regularly employ strong verification techniques on industrial-scale software systems.

"Software Static Code Analysis Lessons Learned"
Andy German, QinetiQ Ltd. CrossTalk Magazine, November 2003
Abstract
The United Kingdom Ministry of Defense has been in the forefront of the use of software static code analysis methodologies, including some of the tools and their application. This article1 discusses what is meant by static analysis, reviews some of the tools, and considers some of the lessons learned from the practical application of software static code analysis when used to evaluate military avionics software.

"Correctness by Construction: Better Can Also Be Cheaper" (PDF 312kb) Peter Amey, Praxis. CrossTalk Magazine, March 2002.
Abstract
For safety and mission critical systems, verification and validation activities frequently dominate development costs, accounting for as much as 80 percent in some cases. There is now compelling evidence that development methods that focus on bug prevention rather than bug detection can both raise quality and save time and money. A recent large avionics project reported a four-fold productivity and 10-fold quality improvement by adopting such methods. A key ingredient of correctness by construction is the use of unambiguous programming languages that allow rigorous analysis very early in the development process.

"Correctness By Construction: Developing a Commercial Secure System" (PDF 358kb)
Anthony Hall and Roderick Chapman, IEEE Software, Jan/Feb 2002, pp18-25
Important Note:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

"Is Proof More Cost Effective Than Testing?" (PDF 677kb)
Steve King, Jonathan Hammond, Rod Chapman and Andy Pryor,
IEEE Transactions on Software Engineering, Volume 26 Number 8.
A paper, originally appearing in 1999 World Congress on Formal Methods, but re-published in IEEE Transactions on Software Engineering. Considers the use of Z, SPARK and Proof in the SHOLIS project and compares the effectiveness of proof with other, more traditional verification activities.

"Combining Static Worst-Case Timing Analysis and Program Proof"
Roderick Chapman, Alam Burns, Andy Wellings. Real-Time Systems Journal, Volume 11, pp145-171, 1996.

"Information-Flow and Data-Flow Analysis of while-Programs"
Jean-Francois Bergeretti and Bernard A. Carré,
University of Southhampton.
Published in ACM Transactions on Programming Languages and Systems.
Vol 7, No. 1, January 1985.
This paper explores the use of data- and information-flow analysis as an aid to program development and validation, and uses the information-flow relations from while-programs to demonstrate how these relations may be used in writing, testing and updating programs and also how they usefully extend the class of errors that may be discovered through static analysis.

We do not have PDF of this document. The ACM electronic library does have it if you have access to that database.