Module 02489 (2012)

Module Description - Automatic Verification

The Module Description is a strict subset of the Syllabus Page, which gives more information

Module TitleAutomatic Verification
SchoolComputer Science
Module Code06-02489
DescriptorCOMP/06-02489/LH
Member of StaffManfred Kerber:5, Unassigned:5
LevelH
Credits10
Semester2
Pre-requisitesNone
Co-requisitesNone
RestrictionsNone
Contact hours25
Delivery18 hrs lectures, 7 hrs examples classes/practical sessions
DescriptionThe 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
AssessmentSessional: 1.5 hr examination (100%).
Supplementary (where allowed): As the sessional assessment
TextsBeatrice Berard et al, Systems and Software Verification: Model-Checking Techniques and Tools Symbolic model checking, 2001
M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed, 2004
Edmund M. Clarke, Orna Grumberg, Doron A. Peled, Model Checking, 2000