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
- http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/
- 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
- http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html
-
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 -- 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
-
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):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.
-
http://www.cl.cam.ac.uk/users/jrh/papers/dijkstra.html
-
SPARK programming language.
- Praxis High Integrity Systems Ltd
-
http://en.wikipedia.org/wiki/SPARK_programming_language