School of Computer Science

Module 06-30211 (2022)

Computer-Aided Verification

Level 3/H

Semester 1 20 credits
Co-ordinator: David Parker
Reviewer: Alan Sexton

The Module Description is a strict subset of this Syllabus Page.

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

  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

Programmes containing this module