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]