University of Birmingham School of Computer Science
Home double arrow Internal double arrow Modules

MODULE DESCRIPTION, 2006/07

06-02489
Automatic Verification

This School of Computer Science Module Description is a strict subset of the Syllabus Page, which gives more information.

Course Code 06-02489
Title Automatic Verification
Code COMP/06-02489/LH
School/Department Computer Science
Member of Staff Prof. M Z Kwiatkowska
Level H
Credits 10
Semester 2
Restrictions None
Pre-requisites None
Co-requisites None
Contact hours 25
Delivery 18 hrs lectures, 7 hrs examples classes/practical sessions
Description The module introduces techniques and tools for verifying that computer systems have the properties intended. The module covers: reactive systems and their models; temporal logic; model checking and algorithms; a selection of tools; examples of systems (concurrent programs, communication protocols, embedded systems); verification of properties of systems (safety, liveness and fairness); the state explosion problem and approaches to it; symbolic model checking.
Outcomes
On successful completion of this module, the student should be able to: Assessed by:
use appropriate tools to verify and debug small-scale systems; Examination
understand and explain the principles and algorithms behind those tools; Examination
explain the application of the tools to the examples introduced; Examination
appreciate the limitations of current techniques and tools, such as the state explosion problem, and current efforts to overcome them. Examination
Assessment Sessional: 1.5 hr examination (100%).
Supplementary (where allowed): As the sessional assessment.
Other -
Texts Beatrice Berard et al, Systems and Software Verification: Model-Checking Techniques and Tools Symbolic model checking, Springer, 2001.
M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed, Cambridge University Press, 2004.
Edmund M. Clarke, Orna Grumberg, Doron A. Peled, Model Checking, The MIT Press, 2000.