Module 02489 (2012)
Syllabus page 2012/2013
06-02489
Automatic Verification
Level 3/H
Unassigned:5
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus
The Module Description is a strict subset of this Syllabus Page. (The University module description has not yet been checked against the School's.)
Changes and updates
This module is not offered in 2012/2013
Relevant Links
Outline
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.
Aims
The aims of this module are to:
- introduce some methods and tools which have been developed in recent years for verifying properties of hardware and software systems
- look at examples, both small-scale ones for classroom demonstration, and large-scale ones in which verification has been successful
- understand the limitations of current tools, and how they may be overcome in the future
Learning Outcomes
| On successful completion of this module, the student should be able to: | Assessed by: | |
| 1 | use appropriate tools to verify and debug small-scale systems | Examination |
| 2 | understand and explain the principles and algorithms behind those tools | Examination |
| 3 | explain the application of the tools to the examples introduced | Examination |
| 4 | appreciate the limitations of current techniques and tools, such as the state explosion problem, and current efforts to overcome them | Examination |
Restrictions, Prerequisites and Corequisites
Restrictions:
None
Prerequisites:
None
Co-requisites:
None
Teaching
Teaching Methods:
18 hrs lectures, 7 hrs examples classes/practical sessions
Contact Hours:
Assessment
- Sessional: 1.5 hr examination (100%).
- Supplementary (where allowed): As the sessional assessment
Recommended Books
| Title | Author(s) | Publisher, Date |
| Systems and Software Verification: Model-Checking Techniques and Tools Symbolic model checking | Beatrice Berard et al | Springer, 2001 |
| Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed | M. Huth and M. Ryan | Cambridge University Press, 2004 |
| Model Checking | Edmund M. Clarke, Orna Grumberg, Doron A. Peled | The MIT Press, 2000 |
Detailed Syllabus
-
Introduction to model checking
- Reactive systems
- Transition system models
- Invariant and reachability checking
- The logic CTL
- CTL model checking
- Real-time and probabilistic systems
- Symbolic model checking and BDDs
- Software model checking
- Foundational issues
- Assertions
- Stateful models
- Predicate transformers
- Interaction models
- On-the-fly checking
- Abstraction and iterated refinement
Last updated: 7 Feb 2007
Source file: /internal/modules/COMSCI/2012/xml/02489.xml
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus