University of St Andrews

Key information

SCOTCAT credits : 15

ECTS credits : 7

Level : SCQF level 10

Semester: 1

Planned timetable: TBC

Building on earlier coverage of elementary logic, this module covers the topics of formal proof (including induction), as applied to software specification, validation and verification. A proof assistant such as PVS or Coq will be employed both in lectures and in practical work, and thus, so far as practicable, all results will be presented with a proof in a machine-checked form. Software correctness is thus presented as a matter not of testing but of pre-execution verification. Typical software covered includes functions on inductively defined data types such as those of lists and trees.

Learning and teaching methods and delivery

Weekly contact:

Scheduled learning hours: 28

Guided independent study hours: 122

Assessment pattern

As used by St Andrews:

As defined by QAA
Written examinations : 60%
Practical examinations : 0%
Coursework: 40%

Personnel