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]
 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 WellStructured and
Correct Programs
 S Alagic and M A Arbib,
SpringerVerlag,
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
 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, 1819 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, andA. J. Perlis
 CACM, 22(5):271280, May 1979
 [Controversial article criticising the value of proof of correctness]

SPARK programming language.

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