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

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