Academic Item Menu


This is a workshop course aimed at developing the skills of writing precise specifications of programs and translating these specifications into correct implementations. The course applies the rigorous modelling and verification techniques introduced in COMP2111 to a diverse and increasingly complex set of problems. Further methods for reasoning about programs are introduced, including methods for reasoning about termination,  program refinement and data refinement. The primary learning outcome is to develop students' abilities to apply these ideas to structure their thinking about programs, but the course may use a formal verification tool to support learning.

Study Level


Offering Terms

Term 3



Delivery Mode

Fully on-site

Indicative contact hours


Conditions for Enrolment

Course Outline

To access course outline, please visit:


Pre-2019 Handbook Editions

Access past handbook editions (2018 and prior)

Helpful utilities like sharing or printing this page
Share Link via Email
Download PDF