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: http://www.cs.bham.ac.uk/research/lics/
[Buy this if you buy anything; also good for the course Temporal Logic and Model Checking.
 Sometimes can be found online using Google]

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 free download from
http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html
[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
http://rsta.royalsocietypublishing.org/content/363/1835/2335.long

Social processes and the proofs of theorems and programs
R. A. DeMillo, R. J. Lipton, and A. J. Perlis
CACM, 22(5):271--280, May 1979
[Controversial article criticising the value of proof of correctness]
http://www.csee.umbc.edu/courses/undergraduate/CMSC331/resources/papers/proofs.pdf

SPARK programming language.
http://en.wikipedia.org/wiki/SPARK_programming_language
[Industrial tool based on generating verification conditions]