Systems Verification (303)
Lectures: Prof.
Alessio Lomuscio,
Dr Panagiotis Kouvaros
Tutorials: Mr Michael Akintunde, Ms Yi-Ling Liu, Prof Alessio
Lomuscio, Mr Edoardo Pirovano.
Lecture Schedule
- Monday 9am-11am; room 360.
- Thursday 11am-1pm; room 360.
Course summary
The course is broadly divided into 5 parts:
- Specifications via logic-based languages (temporal and
epistemic logics) (approx. 4 hrs).
- Ordered binary decision diagrams and their manipulations
(approx. 4 hrs).
- Model checking temporal/epistemic languages (approx. 6hrs).
- The NuSMV and MCMAS model checkers (approx. 4hrs).
- Bounded model checking, parameterised model checking (approx.
4hrs).
The topics will be covered in succession and will be accompanied by
tutorial classes and labs as appropriate. There will be one assessed
coursework around week 4.
The above is subject to slight changes.
Material
Lecture slides and tutorials (with solutions) will be provided on
doc.materials.
An excellent reference text book for most of the material of the
course is M Huth, M Ryan, Logic in Computer Science. Particularly we
will cover material in chapters 3, 4 and 6.
The book is also directly used in many examples in the lectures and
exercises.
The slides and exercise notes used in class are copyrighted.
They can be freely downloaded and used for revision for students
attending the present course but cannot be used by third parties
without the lecturer's permission.
Detailed course breakdown
(This year's module was considerably shortened)
- 13 January
- Introduction and motivation to the course including learning
objectives, assessment methods. Overview of the course.
- Modal specification languages: syntax and semantics.
- Tutorial 1 (modal syntax and satisfaction).
- 16 January
- Linear Temporal Logic (LTL)
- Tutorial 2 (LTL).
- 20 January
- Branching Time Temporal Logic (CTL).
- Exercises from Tutorial 2 (CTL).
- 23 January
- Temporal Specifications, Temporal Equivalences.
- Tutorial 3 (Temporal Specifications).
- 27 February
- Temporal Specifications.
- Mutual Exclusion Problem.
- The Bit Transmission Problem.
- Coursework.
- 30 January
- Explicit Model Checking.
- Tutorial 4 (Explicit model checking).
- 3 February
- Binary Decision Diagrams.
- Symbolic Model Checking with OBDDs.
- 6 February
- NuSMV tutorial 5 (2hrs tutorial in 210/225)
- 10 February
- NuSMV tutorial 6 (2hrs tutorial in 202/206/210)
- 13 February
- Temporal Epistemic Specifications.
- Tutorial 7 (Binary Decision Diagrams).
- 17 February
- The Bit Transmission Problem revisited.
- The MCMAS model checker.
- 20 February
- 24 February
- Bounded Model Checking.
- Tutorial 9 (Epistemic Specifications).
- 27 February
- Parameterised Model Checking.
- Cutoffs.
- 2 March
- Towards Verification of ML-based AI systems.
- Tutorial 10 (Parameterised Model Checking).
- 5 March
- Revision Lecture.
- Q&A Session.