SYLLABUS PAGE, 2006/07
06-02489
Automatic Verification
Level 3/H
|
Prof. M Z Kwiatkowska Dr D R Ghica |
10 credits in Sem2 |
Programmes | Modules | Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus
The School of Computer Science 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
Small changes made to Learning Outcomes and Summary.
Relevant Links
Notes for Prof. Kwiatkowska's section (also available from the lecturer).
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:
| 25 |
Assessment
Normal (sessional): 1.5 hr examination (100%).
Resit (supplementary) (where allowed): As the normal 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
Programmes | Modules | Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus