University of St Andrews

Key information

SCOTCAT credits : 15

ECTS credits : 7

Level : SCQF level 10

Semester: 2

Availability restrictions: Not automatically available to General Degree students

Planned timetable: To be arranged.

Building on earlier coverage of elementary logic, this module motivates the need for formal methods and software verification approaches as model checking for guaranteeing the correctness of software systems. The module covers modelling, system property specification using temporal logics, and more applied approaches to software specification and verification through the use of model checkers. Model checkers such as SPIN and UPPAAL are used both in lectures and in practical work. Petri nets and program semantics are also explored. Software correctness is thus presented as a matter not of testing but of pre-execution verification through model checking.

Relationship to other modules

Pre-requisite(s): Before taking this module you must pass CS3052

Learning and teaching methods and delivery

Weekly contact: 2 hr x 10 weeks lectures, 1 hr x 5 weeks tutorial/discussion.

Assessment pattern

As used by St Andrews: 3-hour Examination = 40%, Coursework = 60%


Re-assessment: 3-hour Examination = 40%, Existing Coursework = 60%

Personnel

Module teaching staff: TBC Module coordinator(s): Honours Coordinator - Computer Science (hons-coord-cs@st-andrews.ac.uk)