Where indicated, PDF downloads of these publications are
available for download here. Where PDF is not available, please
for how to obtain hardcopies.
"Proving SPARK Verification Conditions with SMT solvers"
Paul B. Jackson, Grant Olney Passmore, December 2009.
An Integrated Approach to High Integrity Software Verification
Ireland, Ellis, Chapman, et al.
"Panellist position statement: some industrial experience with program
verification"
Roderick Chapman, Praxis High Integrity Systems
Philosophical Transactions of the Royal Society, October 2005
Click here for an 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
Click here for an 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" 
/ 312kb PDF
Peter Amey, Praxis. CrossTalk Magazine, March 2002.
Click here for an 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"
/ 358kb PDF
Anthony Hall and Roderick Chapman, IEEE Software, Jan/Feb
2002, pp18-25
Click here for an 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?" / 677kb PDF
Steve King, Jonathan Hammond, Rod Chapman and Andy Pryor,
IEEE Transactions on Software Engineering, Volume 26 Number
8.
Click here for an abstract...
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.