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.

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.

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.

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.

Please see Talis Aspire link for most up to date list.

View reading list on Talis Aspire

- Formal reasoning about computer systems, languages and proofs
- Using software systems for formal verification and logic programming

- Capturing statements in natural language as formal mathematical statements
- Understand the limits of computation/proofs

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 |

- background reading
- work on exercise sheets
- programming experiments

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.

Weighting | Study time | |
---|---|---|

Class test | 10% | |

45 minute class test |
||

Practical Coursework | 15% | |

CS262 exam | 75% | |

~Platforms - AEP |

Weighting | Study time | |
---|---|---|

CS262 resit exam | 100% | |

CS262 resit exam ~Platforms - AEP |

Written feedback on coursework.

Verbal feedback in seminars.

This module is Core for:

- Year 2 of UCSA-G500 Undergraduate Computer Science
- Year 2 of UCSA-G503 Undergraduate Computer Science MEng
- Year 2 of UCSA-I1N1 Undergraduate Computer Science with Business Studies
- Year 2 of UCSA-G5N1 Undergraduate Computer and Management Sciences

This module is Optional for:

- Year 2 of USTA-G1G3 Undergraduate Mathematics and Statistics (BSc MMathStat)
- Year 2 of USTA-GG14 Undergraduate Mathematics and Statistics (BSc)

This module is Core option list A for:

- Year 2 of UCSA-G5N1 Undergraduate Computer and Management Sciences

This module is Option list A for:

- Year 2 of UCSA-G400 BSc Computing Systems
- Year 2 of UCSA-G402 MEng Computing Systems
- Year 2 of UCSA-G4G3 Undergraduate Discrete Mathematics

This module is Option list B for:

- Year 2 of UCSA-G4G1 Undergraduate Discrete Mathematics
- Year 2 of UCSA-G4G3 Undergraduate Discrete Mathematics
- Year 2 of UMAA-G105 Undergraduate Master of Mathematics (with Intercalated Year)
- Year 2 of USTA-G300 Undergraduate Master of Mathematics,Operational Research,Statistics and Economics
- Year 2 of UMAA-G100 Undergraduate Mathematics (BSc)
- Year 2 of UMAA-G103 Undergraduate Mathematics (MMath)
- Year 2 of UMAA-G106 Undergraduate Mathematics (MMath) with Study in Europe
- Year 2 of UMAA-G1NC Undergraduate Mathematics and Business Studies
- Year 2 of UMAA-G1N2 Undergraduate Mathematics and Business Studies (with Intercalated Year)
- Year 2 of UMAA-GL11 Undergraduate Mathematics and Economics
- Year 2 of UECA-GL12 Undergraduate Mathematics and Economics (with Intercalated Year)
- Year 2 of UMAA-G101 Undergraduate Mathematics with Intercalated Year
- Year 2 of USTA-Y602 Undergraduate Mathematics,Operational Research,Statistics and Economics