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.

Learning Outcomes

By the end of the module students 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.