Worseand spreading the effect of software flaws far beyond the original customer several devastating computer viruses have taken advantage of bugs and defects in common operating systems such as those sold by Microsoft, hobbling thousands of corporate computer networks last year.
[From an article on CNET on August 27, 2002]
Summary: Program specification: partial and total correctness. Hoare notation. Axioms and rules of FloydHoare logic. Discussion of soundness and completeness. Mechanised program verification: verification conditions. Program refinement. Semantic embedding in higher order logic.
Reading:
Postscript slides (these may change during the course)



Introduction  A3 for projection  A4 for printing 
Formal Specification  A3 for projection  A4 for printing 
Proof Rules for Partial Correctness  A3 for projection  A4 for printing 
Making Proofs Easier  A3 for projection  A4 for printing 
Mechanizing Program Verification  A3 for projection  A4 for printing 
Proving Programs Terminate  A3 for projection  A4 for printing 
Devising Correct Rules  A3 for projection  A4 for printing 
Program Refinement  A3 for projection  A4 for printing 
Higher Order Predicate Calculus  A3 for projection  A4 for printing 
Deriving Floyd Hoare Logic  A3 for projection  A4 for printing 
VDM, Weakest Preconditions, Dynamic Logic  A3 for projection  A4 for printing 



Complete set of slides for printing (4 per page, A4 size)
Examples/Tutorial classes: There are not enough supervisors
to provide supervisions for everyone, so two afternoon examples class
will be run by Joe
Hurd. The first class will be 2pm to 4pm on Monday 24 November in
FW11 (note: this is on a Monday, even though I previously announced
the examples classes would be on Fridays).
Joe will conduct a second class in FW11 at 2pm on Monday 1 December.
Some worked examples
and remarks on answering examination questions will also be given in
the lectures.
Interesting links
Related course: This course is a prerequisite for Specification and Verification II (web page not yet updated for 2004).
Acknowledgement: Some of the teaching materials in this course were prepared by Dr Paul Curzon.
Feedback: If high lecturing standards are to be maintained and lower standards to be raised, it is important for lecturers to receive feedback about their lectures. Consequently, we would be grateful if you would complete this questionnaire. A digest of the information will be passed to the StaffStudent Liaison and Teaching Committees.