Module 06-30211 (2022)

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.

• 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

• 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

2 hr/week lectures

Contact Hours: 34

• Assessments: Examination (80%), Continuous Assessment (20%)
• Supplementary (where allowed): Examination only (100%)

1. Introduction to formal verification
2. Labelled transition systems
3. Modelling sequential and parallel systems
4. Temporal Logic, including LTL and CTL
5. Model checking algorithms
6. Model checking software tools
7. Static analysis & software verification
8. Quantitative verification
9. Selected advanced topics