The University of Sheffield
Department of Computer Science

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 2020/21
Credits 15
Assessment Formal Exam
Lecturer(s) Dr Andrei Popescu
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.