In short, the course was a huge interest booster marred by poor management by the administration team.
This course serves to be the more practical side of theoretical computer science course. The original plan was to be introduced to a range of verification model checkers, such as SPIN/Promela, nuSMV, and SLAM/CBMC which helps to verify algorithms to solve different tasks (including satisfiability and LTL model checking). The theory of the course introduces students to concepts in modern day static analysis and logic in time (temporal logic), which is crucial to algorithmic verification (hence, the name of the course).
The theory was interesting and has definitely been one of the better computer science courses as far as the content goes. Although there wasn't a lot of mathematical concepts, I found myself enjoying the study on topology of behaviour spaces and found that engaging. The assignments weren't too hard and it definitely helped grasp the concepts of the course a lot better.
However, this course has been a nightmare to manage and study for. Assignments were released late, tutorial problem solutions weren't released at all (or at least, they were released extremely late). As a result, assignment marks were released extremely late. Assignment 1 marks were released a few hours before the