Reading list (optional)
Specification and Verification I

Programming from Specifications (2nd Edition)
Carroll Morgan, Prentice Hall International Series in Computer Science, 1994.
Revised edition available for download from

The formal semantics of programming languages: an introduction
Glynn Winskel, MIT Press, 1993.
[Library Location: UL: South Front, Floor 4, Classmark: 348:8.c.95.2645, Status: Not On Loan]

The Design of Well-Structured and Correct Programs
S Alagic and M A Arbib, Springer-Verlag, 1978.
[Nice book, but hard to find]

Semantics with Applications: A Formal Introduction
Hanne Riis Nielson, Flemming Nielson
Wiley Professional Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992.
Revised edition available for download from

Logic in Computer Science: Modelling and Reasoning about Systems
Michael Huth, Mark Ryan
Cambridge University Press, Second Edition 2004. ISBN: 0 521 54310.
Web page:
[Buy this if you buy anything -- good for Specification & Verification II also]

Mechanizing Proof: computing, risk and trust
Donald MacKenzie
MIT Press, 2001. ISBN: 0 262 13393 8.
[Discusses philosophical and social issues]

Computing and the Cultures of Proving
Donald MacKenzie
Paper for Royal Society Discussion Meeting on the Nature of Mathematical Proof,
London, 18-19 October, 2004

Social processes and the proofs of theorems and programs
R. A. DeMillo, R. J. Lipton, andA. J. Perlis
CACM, 22(5):271--280, May 1979

Formalizing Dijkstra.
John Harrison
Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics,
TPHOLs'98, Springer LNCS 1497, pp. 171-188, 1998.

SPARK programming language.
Praxis High Integrity Systems Ltd