Module 06-28201 (2019)

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.

• 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.

1. use appropriate tools to verify, analyse and debug small-scale systems
2. understand and explain the principles and algorithms behind those tools
3. explain the application of the tools to the examples introduced
4. appreciate the limitations of current techniques and tools, such as the state explosion problem, and current efforts to overcome them

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

2 hr/week lectures, 1 hr/week tutorial

Contact Hours:

34

Sessional: 1.5 hr Examination (80%) Continuous Assessment (20%)

Supplementary (where allowed): 1.5 hr examination only

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