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