COM4507 Software and Hardware Verification
Summary 
This module introduces stateoftheart software and
hardware verification techniques which nowadays are widely
used in industry. They are particularly important in
safetycritical applications, where system failures can not
be tolerated. Designing high quality dependable computing
systems is widely believed to be the main challenge in
computer science. Particular focus is on protocol
verification and hardware design verification by model
checking and program verification by formalisms such as
Hoare logics. These techniques presume formal system
specifications and use automated tools for analysing whether
a system satisfies the properties required or imposed. Students should be aware that there are limited places available on this course. 
Session 
Spring 2023/24 
Credits 
15 
Assessment 
Formal Exam 
Lecturer(s) 
Prof. Georg Struth 
Resources 

Aims 
 To develop an understanding of hardware design and
protocol verification by model checking as well as
program verification by formalisms such as Hoare logics
and separation logic
 To study model checking concepts such as temporal
logic formulas, state space, reachability algorithms,
automata theory, BDD algorithms, principles of hardware
verification, and examine case studies with Promela and
SPIN.
 To study program development and verification
concepts like: assertions (pre and postconditions,
invariants), Hoare logics and simple programming
constructs, partial and total correctness, separation
logic
 To discuss current research topics in hardware and
software verification.

Learning Outcomes 
By the end of this module, a candidate will be able to
 Understand the fundamental theory underlying hardware
and software verification
 Appreciate the scope, potential and limitations of
hardware and software specification and verification
 Be able to construct formal specifications for
hardware and software systems, develop appropriate
verification mechanisms and algorithms
 Utilise adequate tools and languages to formally
verify hardware and software systems
 Develop his/her capacity to specify, analyse, verify
and reason about different computing systems
 Have an understanding of current hardware and software
verification research problems and topics

Content 
 Week 1: Introduction and automatatheoretic background
 Week 25: Automatabased and symbolic model checking
(linear temporal logic, Buchi automata, BDDs, model
checking algorithms)
 Week 610: Program verification based on theorem
proving (Hoare logic, partial and total correctness
semantics, interactive theorem proving, refinement,
separation logic)

Teaching Method 
2 formal lectures plus 1 exercise/tutorial session per week. 
Feedback 
Weekly feedback is provided in the exercise/tutorial sessions. 
