Module 28201 (2019)

Module description - Computer-Aided Verification

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

Module Title	Computer-Aided Verification
School	School of Computer Science
Module Code	06-28201
Level	3/H
Member of Staff	Vincent Rahli
Semester	Semester 2 - 10 credits
Delivery	2 hr/week lectures, 1 hr/week tutorial Contact Hours: 34
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.
Outcomes	On successful completion of this module, the student 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
Assessment	Sessional: 1.5 hr Examination (80%) Continuous Assessment (20%) Supplementary (where allowed): 1.5 hr examination only