Aims and objectives:

Lecture notes for High Integrity Computing:

• Introduction
• Tools and Techniques Overview
• The SPARK Approach - Part 1
• The SPARK Approach - Part 2
• Flow Analysis - How It Works
• Program Specification
• Verification Condition Generation
• Program Proof
• Exception Freedom Proof
• Proof By Mathematical Induction
• Faults, Failures and Reliability
• Summary

Web Based Resources:

• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Proof Designer by Daniel J. Velleman

Additional module material:

• Notes
• Code
• Exercises
• Solutions

Assignment for F23PS2:

• Assignment Specification
• Assignment Test Data [ available ]
• Assignment Grades [ available ]

Assignment for F29HD2:

• Assignment Specification
• Assignment Test Data [ available ]
• Assignment Grades [ available ]

Recommended reading:

• Amey, P. Correctness by Construction: Better Can Also Be Cheaper, Praxis Critical Systems Limited. CrossTalk Magazine, March 2002.
• Barnes, J. High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley, 2003, ISBN 0-321-13616-0.
• Bundy, A. and Basin, D. and Hutter, D. and Ireland, A. Rippling: Meta-level Guidance for Mathematical Reasoning, Cambridge University Press, 2005.
• Chapman, R. and Amey, P. Industrial Strength Exception Freedom, Proceedings of ACM SigAda 2002.
• King, S. Hammond, J. Chapman, J. Pryor, A. Is Proof More Cost-Effective Than Testing? IEEE Transactions on Software Engineering, Vol 26(8), 2000.
• Ross, P.E. The Exterminators IEEE Spectrum, Sept 2005.
• Storey, N. Safety-Critical Computer Systems, Addison-Wesley, 1996.
• ESC/Java2: Publications.
• Spec#: Publications.
• Ada Europe
• The World Wide Web Virtual Library: Formal Method
• Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems, Volume II: A Practitioner's Companion [NASA-GB-001-97], Published by NASA, 1997
• The Risks Digest
• SPARK Resource [ Praxis Critical Systems Ltd ]