The module introduces the student to the use of logic as a tool for specifying the desired behavior of hardware, software and artificial intelligence systems, and for checking whether a given system does indeed behave as desired. The module enables the student to gain familiarity with a set of techniques which are critical in contemporary industrial applications and in academic research. It consists of 30 lectures and 10 practical sessions.