Reading list (optional)

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 -- also good for the course Temporal Logic and Model Checking]

The formal semantics of programming languages: an introduction
Glynn Winskel, MIT Press, 1993.
[Excellent for the soundness and completeness of Hoare logic]

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 freee download from
[Chapter 6 may be useful]

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
[Controversial article criticising the value of proof of correctness]

SPARK programming language.
[Industrial tool based on generating verification conditions]