SYSTEMS VERIFICATION  2020/1
Module code: COM3028
Module Overview
The course is an introduction in formal methods for system specification and verification.
It will focus on logicbased formalisms and techniques, and specifically on model checking.
The main logics taught will be temporal logics, which are mainstream in verification, especially analysis of hardware systems.
Other logics and verification techniques (such as theorem proving) will be included to a smaller extended.
Model checkers will be used in the labs, on different systemverification problems.
Elements of building model checking tools will be presented and explored.
Some elements of advanced verification techniques (e.g., abstraction) will be mentioned.
Module provider
Computer Science
Module Leader
BOUREANU IC Dr (Computer Sci)
Number of Credits: 15
ECTS Credits: 7.5
Framework: FHEQ Level 6
JACs code: I100
Module cap (Maximum number of students): N/A
Module Availability
Semester 2
Prerequisites / Corequisites
Basic discrete maths (sets, functions, etc.)  COM1026 Basic propositional calculus  COM1026 Basic firstorder logic  COM1026 Basic C/C++ programming  COM2040
Module content
The content (topics of lectures, tutorials and labs) follow:
1. Introduction + Introduction to System Verification
2. Basic Modal Concepts
Tutorial  Modal specifications and satisfaction
3. The logics LTL and CTL
Tutorial  LTL and CTL
4. The logics LTL vs CTL cont'd (expressivity) + The logic of CTL*
Tutorial 3  LTL and CTL (cont’d)
5. Advanced Temporal Specifications Examples
Lab  on the introduction to a model checker
6. SystemModelling Examples
7. Explicit Model Checking
Tutorial  Explicit model checking
8. Binary Decision Diagrams (BDDs)
Tutorial  Binary Decision Diagrams
Lab  on using/manipulating BDDs
9. Symbolic Model Checking
Lab 3  on further, more advanced usage of a model checker
10. Nonclassical Logics  Part I
11. Nonclassical Logics  Part II
12. Revision week
Assessment pattern
Assessment type  Unit of assessment  Weighting 

Examination  Final exam  50 
Coursework  Coursework 1  25 
Coursework  Coursework 2  25 
Alternative Assessment

Assessment Strategy
The assessment strategy is designed to provide students with the opportunity to demonstrate that they have achieved the module learning outcomes.
Thus, the summative assessment for this module consists of:
· First individual coursework on temporal logic and explicit model checking. This addresses LO1 and LO2.
· Second individual coursework on temporal logic, explicit and symbolic model checking and the use of the latter techniques in practice. This addresses LO1, LO2 and LO3.
· A 2h unseen examination on the whole course content. This addresses LO1, LO2, LO3, LO4.
The individual pieces of coursework will be due around week 5 and 10 respectively. The exam takes place at the end of the semester during the exam period.
Formative assessment and feedback
1. PollEverywhere will be used in the lectures with each lecture consisting of a number of slides explaining the theory followed by a number of slides gauging the students’ understanding. The answers are discussed when necessary, e.g., if a high proportion (more than 25%) of the students got the answer wrong.
2. Individual formative feedback will also be given during the lab sessions, and as part of the summative assessment.

Assessment & Assessment Strategy: Executive Summary
Coursework 1 (25%)  takehome work, testing learning outcomes 1 and 2
Coursework 2 (25%)  takehome work, testing learning outcomes 1 and 2 and 3
Final exam (50%)  unseen written piece of examination in the exam period, testing learning outcomes 1 and 2 and 3 and 4
Labs (Formative)  carried out in the labs at the university, focusing on learning outcomes 2 and 3
Module aims
 Introducing formal methods for system specification and verification
 Focus on logicbased techniques for system verification, particularly model checking
 Give a flavour of advanced model checking techniques and of other verification methods, such as theorem proving
Learning outcomes
Attributes Developed  

001  Understand the use of temporal logic and, to some extend, other logics as formal specification languages  KCT 
002  Understand and use verification algorithms such as the ones based on SAT (satisfiability of logic formulae) and/or using orderedbinarydecision diagrams  KCPT 
003  Learn how to use of a model checker and, potentially, a theorem prover to verify systems against formal specifications  KCP 
004  Appreciate the limitations of current techniques and develop a basic understanding of research directions in this space  KC 
Attributes Developed
C  Cognitive/analytical
K  Subject knowledge
T  Transferable skills
P  Professional/Practical skills
Overall student workload
Independent Study Hours: 110
Lecture Hours: 24
Tutorial Hours: 10
Laboratory Hours: 6
Methods of Teaching / Learning
The learning and teaching strategy is designed to develop a critical understanding of the foundations of systems verification, facilitating selfdirected further studying in this field.
The skills learned in this module will be transferable to other verification techniques, such as program analysis.
Also developing critical thinking is at the core of this module.
The learning and teaching methods include:
Twentyfour hours of lectures with class discussion
Ten hours of tutorials
Six hours of lab classes
Use of an online forum for facilitated discussion
Indicated Lecture Hours (which may also include seminars, tutorials, workshops and other contact time) are approximate and may include inclass tests where one or more of these are an assessment on the module. Inclass tests are scheduled/organised separately to taught content and will be published on to student personal timetables, where they apply to taken modules, as soon as they are finalised by central administration. This will usually be after the initial publication of the teaching timetable for the relevant semester.
Reading list
Reading list for SYSTEMS VERIFICATION : http://aspire.surrey.ac.uk/modules/com3028
Other information
REFERENCES:
 Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York, NY, USA.
 Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics: With Isabelle/HOL. Springer Publishing Company.
 Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. 2003. Reasoning about Knowledge. MIT Press, Cambridge, MA, USA.
Programmes this module appears in
Programme  Semester  Classification  Qualifying conditions 

Computer Science BSc (Hons)  2  Optional  A weighted aggregate mark of 40% is required to pass the module 
Computing and Information Technology BSc (Hons)  2  Optional  A weighted aggregate mark of 40% is required to pass the module 
Please note that the information detailed within this record is accurate at the time of publishing and may be subject to change. This record contains information for the most up to date version of the programme / module for the 2020/1 academic year.