Computer Laboratory > Teaching > Course material 2008–09 > Computer Science Tripos Syllabus and Booklist 2008-2009 > Specification and Verification I

next up previous contents
Next: Specification and Verification II Up: Lent Term 2009: Part Previous: Natural Language Processing   Contents


Specification and Verification I

Lecturer: Professor M.J.C. Gordon

No. of lectures: 12

Prerequisite course: Logic and Proof

This course is a prerequisite for Specification and Verification II.

Aims

The aim of the course is to motivate and illustrate the use of rigorous methods and mechanised tools for reasoning about the functional behaviour of imperative programs. A goal is to show the similarities and differences between hardware and software verification.

Lectures

Objectives

By the end of the course students should have an understanding of some aspects of the following topics. Partial and total correctness. Hoare notation. Axioms and rules of Floyd-Hoare logic. Soundness and completeness. Mechanised program verification using verification conditions. Program refinement. Semantic embedding in higher order logic. Limitations of program verification.

Recommended reading

Comprehensive notes supplied.



next up previous contents
Next: Specification and Verification II Up: Lent Term 2009: Part Previous: Natural Language Processing   Contents