Module description
Aims and Learning Outcomes
This module aims at providing an in-depth introduction to different state-of-the-art methodologies of Formal Verification and the applications of those methodologies to formally model and reason about algorithms, software, systems, and protocols.
On successful completion of this module, students will be able to:
- Define a range of formal models
- Formalise problems and specify properties to be verified
- Apply different methods and algorithms for verification
Syllabus
Topics on the module include:
- Formal logics and modelling in formal logics.
- Methods and techniques to reason about formal models.
- Applications of formal verification to hardware, software, and security verification.
- Hands-on usage of verification tools.
Assessment details
Please note: The below assessment details for the 2025/26 academic year may be updated. The confirmed details will be available on the Student Handbook and on the module KEATS page at the beginning of the semester.
- 70% Examination
- 30% Coursework
Semester 1 only study abroad students will be required to take the exam component in an alternative assessment format in the January exam period.
Full year study abroad students will be required to take this exam in person in January.