Theory of Computation and Formal Verification

Undergraduate | 2026

Course page banner
area/catalogue icon
Area/Catalogue
COMP 2003
Course ID icon
Course ID
200080
Level of study
Level of study
Undergraduate
Unit value icon
Unit value
6
Course level icon
Course level
2
Study abroad and student exchange icon
Inbound study abroad and exchange
Inbound study abroad and exchange
The fee you pay will depend on the number and type of courses you study.
Yes
University-wide elective icon
University-wide elective course
Yes
Single course enrollment
Single course enrolment
Yes
alt
Note:
Course data is interim and subject to change

Course overview

This course delves into the fundamental concepts of computability theory, exploring the boundaries and limitations of algorithmic solutions. Students will examine the classification of algorithmic solutions, studying various types of algorithms and their applicability to different problem domains. The course also covers formal verification techniques, providing learners with the tools to rigorously assess the correctness and reliability of algorithms. This formal lens will also be used to analyse and compare between software development practices.

Course learning outcomes

  • Demonstrate advanced knowledge of formal computation and its relationship to languages
  • Analyse different computing languages and classify their respective types
  • Describe formal reasoning about languages
  • Formalise specifications of various programs
  • Apply the inductive hypothesis in various settings
  • Analyse current software development practices through a formal lens

Prerequisite(s)

Corequisite(s)

N/A

Antirequisite(s)

N/A