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.