# Module 06-28201 (2015)

## Computer-Aided Verification

## Level 3/H

David Parker | Semester 2 | 10 credits |

### Outline

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.

### Aims

The aims of this module are to:

- introduce the basic ideas of automatic verification;
- familiarise the student with key techniques and algorithms for verification;
- illustrate some of the uses and applications of automatic verification;
- give practical experience in using state of the art verification software;
- provide a foundation for further study in the area of formal verification.

### Learning 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

### Restrictions

06-05934 (Models of Computation), A-Level Maths (Or Equivalent)

### Pre-requisites

- 06-05934 - Models of Computation

### Teaching methods

2 hr/week lectures, 1 hr/week tutorial

Contact Hours:

34

### Assessment

Sessional: 1.5 hr Examination (70%) Continuous Assessment (30%, split between 10% on written exercises and 20% on a mini-project assessed by report)

Supplementary (where allowed): (where allowed) 1.5 hr examination (80%) with the mini-project mark carried forward (20%)

### Detailed Syllabus

- Introduction: motivation, aims, organisation, references
- Modelling sequential and reactive systems, Kripke structures
- Temporal logic: CTL, LTL and CTL*
- Property specification with temporal logic
- Tools for model checking
- Symbolic model checking
- Software verification
- Bounded model checking via propositional satisfiability
- Symbolic execution
- Model checking for real-time system
- Model checking for probabilistic systems
- Advanced applications, e.g., computer security, robotics
- Verification (and related) software, e.g.: Nu-SMV, SPIN, ProB,FDR, Z3, UPPAAL, PRISM, ProVerif

### Programmes containing this module

- BSc Artificial Intelligence & Computer Science [0144]
- BSc Artificial Intelligence & Computer Science with an Industrial Year [9502]
- BSc Artificial Intelligence & Computer Science with Study Abroad [452B]
- BSc Computer Science [4436]
- BSc Computer Science with an Industrial Year [9499]
- BSc Computer Science with Study Abroad [5571]
- BSc Mathematics and Computer Science [5196]
- BSc Mathematics and Computer Science with an Industrial Year [9495]
- MEng Computer Science/Software Engineering [4754]
- MEng Computer Science/Software Engineering with an Industrial Year [9501]
- MSci Computer Science [4443]
- MSci Computer Science with an Industrial Year [9509]
- MSci Computer Science with Study Abroad [5576]
- MSci Mathematics and Computer Science [5197]
- MSci Mathematics and Computer Science with an Industrial Year [9496]
- MSci Pure Mathematics and Computer Science [5256]
- MSci Pure Mathematics and Computer Science with an Industrial Year [9498]