Computer-Aided Formal Verification

Overview

Computer-aided formal verification aims to improve the quality of digital systems by using logical reasoning, supported by software tools, to analyse their designs. The idea is to build a mathematical model of a system and then try to prove properties of it that validate the system's correctness - or at least help discover subtle bugs. The proofs can be millions of lines long, so specially-designed computer algorithms are used to search for and check them.

This course provides an in-depth survey of several major software-assisted verification methods, covering both theory and practical applications. The aim is to familiarise students with the mathematical principles behind current verification technologies and give them an appreciation of how these technologies are used in industrial system design today. The application focus is on formal verification of hardware designs, currently the most successful application of computer-aided verification. The course does not, however, require advanced background knowledge of digital logic or hardware design.