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
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
- 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
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.
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.
2nd ed., Cambridge : Cambridge University Press
Cambridge, Mass. ; London : MIT Press
Istituto Scientifico per lo Studio e la Cura dei Tumori (IRST)