COM4507 Software and Hardware Verification
| Summary |
This module introduces state-of-the-art software and
hardware verification techniques which nowadays are widely
used in industry. They are particularly important in
safety-critical 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 2022/23 |
| Credits |
15 |
| Assessment |
Formal Exam |
| Lecturer(s) |
Dr Andrei Popescu & 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 post-conditions,
invariants), Hoare logics and simple programming
constructs, partial and total correctness, separation
logic
- To discuss current research topics in hardware and
software verification.
|
| Objectives |
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 automata-theoretic background
- Week 2-5: Automata-based and symbolic model checking
(linear temporal logic, Buchi automata, BDDs, model
checking algorithms)
- Week 6-10: 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. |
| Recommended Reading |
A long list of reading material is available from the course web site. |
|
