Programme And Module Handbook
 
Course Details in 2022/23 Session


If you find any data displayed on this website that should be amended, please contact the Curriculum Management Team.

Module Title LM Computer-Aided Verification (Extended)
SchoolComputer Science
Department Computer Science
Module Code 06 30239
Module Lead David Parker
Level Masters Level
Credits 20
Semester Semester 1
Pre-requisites LC Mathematical and Logical Foundations of Computer Science - (06 35324)
Co-requisites
Restrictions None
Contact Hours Lecture-33 hours
Guided independent study-167 hours
Total: 200 hours
Exclusions
Description Showing that computer systems, hardware or software, are free of bugs is an important and challenging area of computer science but is essential in contexts such as safety-critical applications or computer security, where the consequences can be severe. This module introduces the field of formal verification, which rigorously checks the correctness of computer systems. Students will be introduced to the concept of mathematical modelling of systems, both sequential and parallel, learn how to formalise correctness properties using logics, notably temporal logic, and how to verify them automatically using techniques such as model checking. The module will cover both the theory and algorithms underlying these verification techniques and give a practical introduction to using verification tools.
Learning Outcomes By the end of the module students should be able to:
  • Understand and apply basic concepts for mathematical modelling of systems, such as labelled transition systems
  • Express formal correctness properties of systems using logic
  • Use formal verification algorithms, techniques and tools to check properties of systems and explain the principles behind them
  • Demonstrate the capacity to independently study, understand, and critically evaluate advanced materials or research articles in the subject areas covered by this module.
Assessment
Assessment Methods & Exceptions Assessments: Examination (80%), Continuous Assessment (20%)
Reassessment: Examination (100%)
Other
Reading List