If you find any data displayed on this website that should be amended, please contact the Curriculum Management Team.
Module Title
LM Computer-Aided Verification (extended)
School
Computer Science
Department
Computer Science
Module Code
06 28206
Module Lead
David Parker
Level
Masters Level
Credits
10
Semester
Full Term
Pre-requisites
Co-requisites
Restrictions
None
Exclusions
Description
The module introduces techniques and tools for automatically verifying that computer systems behave as intended, in terms of correctness and reliability. The module covers: reactive systems and their models; temporal logic; model checking and algorithms; quantitative model checking; the state explosion problem and approaches to addressing it; examples of systems (e.g., concurrent programs, communication protocols, embedded systems). 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:
use appropriate tools to verify, analyse and debug small-scale systems
understand and explain the principles and algorithms behind those tools
explain the application of the tools to the examples introduced
appreciate the limitations of current techniques and tools, such as the state explosion problem, and current efforts to overcome them