CS4052 Logic and Software Verification

Academic year

2025 to 2026 Semester 2

Further information on which modules are specific to your programme.

Key module information

SCOTCAT credits

15

The Scottish Credit Accumulation and Transfer (SCOTCAT) system allows credits gained in Scotland to be transferred between institutions. The number of credits associated with a module gives an indication of the amount of learning effort required by the learner. European Credit Transfer System (ECTS) credits are half the value of SCOTCAT credits.

SCQF level

SCQF level 10

The Scottish Credit and Qualifications Framework (SCQF) provides an indication of the complexity of award qualifications and associated learning and operates on an ascending numeric scale from Levels 1-12 with SCQF Level 10 equating to a Scottish undergraduate Honours degree.

Availability restrictions

Not automatically available to General Degree students

Planned timetable

To be arranged.

This information is given as indicative. Timetable may change at short notice depending on room availability.

Module Staff

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

This information is given as indicative. Staff involved in a module may change at short notice depending on availability and circumstances.

Module description

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-requisites

BEFORE TAKING THIS MODULE YOU MUST PASS CS3052

Assessment pattern

3-hour Examination = 40%, Coursework = 60%

Re-assessment

3-hour Examination = 40%, Existing Coursework = 60%

Learning and teaching methods and delivery

Weekly contact

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

Scheduled learning hours

26

The number of compulsory student:staff contact hours over the period of the module.

Guided independent study hours

124

The number of hours that students are expected to invest in independent study over the period of the module.