Is Proof More Cost-Effective Than Testing?,Steve King, Jonathan Hammond, Rod Chapman and Andy Pryor, IEEE Transactions on Software Engineering, Vol 26 No 8, pp675–686 (August 2000).

Reports on a safety-critical software development which used formal specification and carried out extensive proof of the specification and of the SPARK code. Demonstrates that proof is a cost-effective means of removing errors, better than some forms of testing.

Industrial-Strength Formal Methods in Practice, M.G. Hinchey & J.P. Bowen, Springer, 1999.

High Integrity System Specification and Design, J.P. Bowen & M.G. Hinchey, Springer, 1999.

Investigating the Influence of Formal Methods, S. Lawrence Pfleeger, L. Hatton. IEEE Computer, February 1997: 33–43.(Available via the Digital Library)

An independent assessment of the impact of formal methods on the development of CDIS. For a description of the project see my IEEE Software paper.