Module 06-30239 (2022)
Computer-Aided Verification (Extended)
Level 4/M
Semester 1 | 20 credits |
Outline
Showing that computer systems, hardware or software, are free of bugs is an important and
challenging area of computer science but is essential in contexts such as safety-critical applications or computer security, where the consequences can be severe. This module introduces the field of formal verification, which rigorously checks the correctness of computer systems. Students will be introduced to the concept of mathematical modelling of systems, both sequential and parallel, learn how to formalise correctness properties using logics, notably temporal logic, and how to verify them automatically using techniques such as model checking. The module will cover both the theory and algorithms underlying these verification techniques and give a practical introduction to using verification tools.
Aims
The aims of this module are to:
- introduce the basic ideas of automatic verification;
- familiarise the student with key techniques and algorithms for verification;
- illustrate some of the uses and applications of automatic verification;
- give practical experience in using state of the art verification software;
- provide a foundation for further study in the area of formal verification.
Learning Outcomes
On successful completion of this module, the student should be able to:
- Understand and apply basic concepts for mathematical modelling of systems, such as labelled transition systems
- Express formal correctness properties of systems using logic
- Use formal verification algorithms, techniques and tools to check properties of systems and explain the principles behind them
- demonstrate the capacity to independently study, understand, and critically evaluate advanced materials or research articles in the subject areas covered by this module.
Pre-requisites
- 06-35324 - Mathematical and Logical Foundations of Computer Science
Teaching methods
2 hr/week lectures
Contact Hours: 34
Assessment
- Assessments: Examination (80%), Continuous Assessment (20%)
- Reassessment: Examination (100%)
Detailed Syllabus
- Introduction to formal verification
- Labelled transition systems
- Modelling sequential and parallel systems
- Temporal Logic, including LTL and CTL
- Model checking algorithms
- Model checking software tools
- Static analysis & software verification
- Quantitative verification
- Selected advanced topics
Programmes containing this module
- MEng Computer Science/Software Engineering [4754]
- MEng Computer Science/Software Engineering with an Industrial Year [9501]
- MSc Advanced Computer Science [0014]
- MSc Cyber Security [504B]
- MSci Computer Science [4443]
- MSci Computer Science with an Industrial Year [9509]
- MSci Computer Science with Study Abroad [5576]
- MSci Mathematics and Computer Science [5197]
- MSci Mathematics and Computer Science with an Industrial Year [9496]