Module 06-30211 (2022)
Computer-Aided Verification
Level 3/H
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
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%)
- Supplementary (where allowed): Examination only (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
- BSc Artificial Intelligence & Computer Science [0144]
- BSc Artificial Intelligence & Computer Science with an Industrial Year [9502]
- BSc Artificial Intelligence & Computer Science with Study Abroad [452B]
- BSc Computer Science [4436]
- BSc Computer Science with an Industrial Year [9499]
- BSc Computer Science with Digital Technology Partnership (PwC) [610C]
- BSc Computer Science with Digital Technology Partnership (Vodafone) [893C]
- BSc Computer Science with Study Abroad [5571]
- BSc Mathematics and Computer Science [5196]
- BSc Mathematics and Computer Science with an Industrial Year [9495]
- MEng Computer Science/Software Engineering [4754]
- MEng Computer Science/Software Engineering with an Industrial Year [9501]
- 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]