Module overview
Aims and Objectives
Learning Outcomes
Knowledge and Understanding
Having successfully completed this module, you will be able to demonstrate knowledge and understanding of:
- Refinement-based approaches to program development
- Deductive reasoning techniques for program correctness
- Model checking as an automated technique for verifying properties of software systems
- The use of logical specifications to formalise program correctness
Subject Specific Intellectual and Research Skills
Having successfully completed this module you will be able to:
- Use a range of verification tools to build correct programs
- Capture statements in natural language as formal mathematical statements
- Understand the workings and limitations of different formal approaches to software correctness
Syllabus
- Propositional and predicate logic, soundness and completeness (mostly recap)
- Pre- and post-conditions, loop invariants, assertions; program contracts
- Proof calculi for program verification (Hoare logic; dynamic logic)
- Modelling (concurrent) programs using transition systems
- Temporal logic (LTL) and verification by model checking
- Refinement-based approaches to program construction (Event-B)
Learning and Teaching
Teaching and learning methods
The content of this module is delivered through lectures, the module website, directed reading, pre-recorded materials and tutorials.
Students work on their understanding through a combination of independent study, preparation for timetabled activities and tutorials, along with formative assessments in the form of coursework assignments.
Type | Hours |
---|---|
Completion of assessment task | 41 |
Lecture | 36 |
Tutorial | 12 |
Wider reading or practice | 25 |
Follow-up work | 18 |
Preparation for scheduled sessions | 6 |
Revision | 12 |
Total study time | 150 |
Assessment
Assessment strategy
This module is assessed by a combination of coursework and a final assessment in the form of a written examination.
Summative
This is how we’ll formally assess what you have learned in this module.
Method | Percentage contribution |
---|---|
Coursework | 40% |
Examination | 60% |