Worse--and 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 Floyd-Hoare logic. Discussion of soundness and completeness. Mechanised program verification: verification conditions. Program refinement. Semantic embedding in higher order logic.
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.
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 Staff-Student Liaison and Teaching Committees.