Systems Verification

Module aims

In this module you will have the opportunity to:

  • study the role of logic and and model checking in systems verification
  • explore compressed representations of logical formulae with a view to improving model checking performance
  • use state-of-the-art model checkers as verification tools
  • explore advanced topics in the verification of AI systems   

Learning outcomes

Upon successful completion of this module you will be able to:

  • use the temporal logics LTL, CTL to specify desired system properties
  • assess the use of formal verification and its limitations
  • use symbolic data structures such as ordered-binary decision diagrams for model checking
  • select and use appropriate model checkers for a given verification problem
  • verify key properties of distributed systems
  • evaluate potential applications of verification in AI systems   

Module syllabus

  • Linear Temporal Logic
  • Branching Time Temporal Logic
  • The model checking decision problem
  • Explicit algorithms for model checking
  • Ordered Binary Decision Diagrams
  • Symbolic model checking
  • Epistemic Specifications
  • The NuSMV and MCMAS model checkers
  • Bounded model checking
  • Abstraction methods
  • Verification of MultiAgent Systems against expressive specifications

Teaching methods

The module is taught through interactive classroom sessions aimed at eliciting a dialogue between lecturer and students. Questions are welcome and sought during the lectures and all students are invited to participate. Exercises will often be chosen by the students themselves. Unassessed, formative exercises form the basis of much of the discussion and the interaction that ensues is an essential part of the teaching and learning philosophy. In addition to face to face discussion with the lecturer  you will also be given paths for self-study of advanced material, should you wish to exlpore topics that lie beyond the core module content. Some of the classroom sessions will be co-supervised by Graduate Teaching Assistants (GTAs).

The Piazza Q&A web service will be used as an open online discussion forum for the module.            

Assessments

The module will feature two coursework components: the first will cover the first half of the course based on the theoretical underpinnings of model checking; the second is a practical modelling and verification exercise.These courseworks together count for 20% of the marks for the module. There will be a final written exam, which will test both theoretical and practical aspects of the subject. This exam counts for the remaining 80% of the marks.       

Written feedback on the coursework submission will be provided. Tutorials are intended to be occasions for providing individual feedback and you will be encouraged to interact with the lecturer and GTAs.

Reading list

Core Reading

Module leaders

Professor Alessio Lomuscio