Introductory description
To give students an understanding of the basics of mathematical logic, and its applications to specifying and verifying computing systems.
This module is only available to students in the second year of their degree and is not available as an unusual option to students in other years of study.
Module aims
To give students an understanding of the basics of mathematical logic, and its applications to specifying and verifying computing systems. Algorithms and proof calculi for verification, as well as associated tools, will be studied. Theory and practice relating to reliability of systems form a vital part of computer science.
Outline syllabus
This is an indicative module outline only to give an indication of the sort of topics that may be covered. Actual sessions held may differ.
 Propositional logic: proofs, semantics, normal forms, SAT solvers.
 Predicate logic: proofs, semantics.
 Specifying and modelling software.
 Verification by model checking.
 Proof calculi for program verification.
Learning outcomes
By the end of the module, students should be able to:
 Construct and reason about proofs in a variety of logics.
 Understand and compare the semantics of a variety of logics.
 Apply logic to specify and verify computing systems.
 Understand basic algorithms for formal verification.
 Use formal verification tools.
Indicative reading list
Please see Talis Aspire link for most up to date list.
View reading list on Talis Aspire
Subject specific skills
 Formal reasoning about computer systems, languages and proofs
 Using software systems for formal verification and logic programming
Transferable skills
 Capturing statements in natural language as formal mathematical statements
 Understand the limits of computation/proofs
Study time
Type 
Required 
Lectures 
30 sessions of 1 hour (20%)

Seminars 
7 sessions of 1 hour (5%)

Practical classes 
3 sessions of 1 hour (2%)

Private study 
110 hours (73%)

Total 
150 hours 
Private study description
 background reading
 work on exercise sheets
 programming experiments
Costs
No further costs have been identified for this module.
You do not need to pass all assessment components to pass the module.
Students can register for this module without taking any assessment.
Assessment group D2

Weighting 
Study time 
Class test

10%


45 minute class test

Practical Coursework

15%


CS262 exam

75%


~Platforms  AEP
 Online examination: No Answerbook required

Assessment group R

Weighting 
Study time 
CS262 resit exam

100%


CS262 resit exam
~Platforms  AEP

Feedback on assessment
Written feedback on coursework.
Verbal feedback in seminars.
Past exam papers for CS262
Courses
This module is Core for:

Year 2 of
UCSAG500 Undergraduate Computer Science

Year 2 of
UCSAG503 Undergraduate Computer Science MEng

Year 2 of
UCSAI1N1 Undergraduate Computer Science with Business Studies

Year 2 of
UCSAG5N1 Undergraduate Computer and Management Sciences
This module is Optional for:

Year 2 of
USTAG1G3 Undergraduate Mathematics and Statistics (BSc MMathStat)

Year 2 of
USTAGG14 Undergraduate Mathematics and Statistics (BSc)
This module is Core option list A for:

Year 2 of
UCSAG5N1 Undergraduate Computer and Management Sciences
This module is Option list A for:

Year 2 of
UCSAG400 BSc Computing Systems

Year 2 of
UCSAG402 MEng Computing Systems

Year 2 of
UCSAG4G3 Undergraduate Discrete Mathematics
This module is Option list B for:

Year 2 of
UCSAG4G1 Undergraduate Discrete Mathematics

Year 2 of
UCSAG4G3 Undergraduate Discrete Mathematics

Year 2 of
UMAAG105 Undergraduate Master of Mathematics (with Intercalated Year)

Year 2 of
USTAG300 Undergraduate Master of Mathematics,Operational Research,Statistics and Economics

Year 2 of
UMAAG100 Undergraduate Mathematics (BSc)

Year 2 of
UMAAG103 Undergraduate Mathematics (MMath)

Year 2 of
UMAAG106 Undergraduate Mathematics (MMath) with Study in Europe

Year 2 of
UMAAG1NC Undergraduate Mathematics and Business Studies

Year 2 of
UMAAG1N2 Undergraduate Mathematics and Business Studies (with Intercalated Year)

Year 2 of
UMAAGL11 Undergraduate Mathematics and Economics

Year 2 of
UECAGL12 Undergraduate Mathematics and Economics (with Intercalated Year)

Year 2 of
UMAAG101 Undergraduate Mathematics with Intercalated Year

Year 2 of
USTAY602 Undergraduate Mathematics,Operational Research,Statistics and Economics