Module overview
This module aims to train students in both the principles and the practice of software verification. A range of verification approaches, including both testing and formal verification, will be covered. The use of logic as a specification language for programs will be explored. In addition to covering the key techniques for software verification, the module will provide practical experience in using state of the art verification tools.
Aims and Objectives
Learning Outcomes
Subject Specific Practical Skills
Having successfully completed this module you will be able to:
- Select appropriate verification tools to analyse and verify small-scale systems
Knowledge and Understanding
Having successfully completed this module, you will be able to demonstrate knowledge and understanding of:
- The use of logic as a specification language for software correctness
- A range of testing and verification approaches applicable to software systems
Subject Specific Intellectual and Research Skills
Having successfully completed this module you will be able to:
- Assess the limitations of current verification techniques and tools
- Apply automated verification techniques to software
Syllabus
Software testing
1.Types of testing
2.Black-box testing
3.Test coverage and structural testing
4.Regression testing
5.Automated test case generation
Formal verification
1.Approaches to modelling software
2.Property specification using temporal logic
3.Model checking
4.Symbolic execution
Learning and Teaching
Teaching and learning methods
The module uses lectures to present the material and tutorials to enhance the understanding of various verification techniques and demonstrate the use of verification tools.
| Type | Hours |
|---|---|
| Lecture | 36 |
| Wider reading or practice | 6 |
| Tutorial | 12 |
| Revision | 15 |
| Completion of assessment task | 45 |
| Preparation for scheduled sessions | 18 |
| Independent Study | 18 |
| Total study time | 150 |
Assessment
Summative
This is how we’ll formally assess what you have learned in this module.
| Method | Percentage contribution |
|---|---|
| Coursework | 20% |
| Coursework | 15% |
| Examination | 65% |
Referral
This is how we’ll assess you if you don’t meet the criteria to pass this module.
| Method | Percentage contribution |
|---|---|
| Examination | 100% |
Repeat
An internal repeat is where you take all of your modules again, including any you passed. An external repeat is where you only re-take the modules you failed.
| Method | Percentage contribution |
|---|---|
| Examination | 100% |
Repeat Information
Repeat type: Internal & External