Skip to main content

Computer-Aided Formal Verification:  2009-2010

Lecturer

Degrees

Schedule C1Computer Science

Part CMathematics and Computer Science

Schedule CMSc in Advanced Computer Science

MSc in Mathematics and Foundations of Computer Science

MSc by Research

Term

Overview

This course introduces the fundamentals of computer-aided formal verification. Computer-aided formal verification aims to improve the quality of digital systems by using logical reasoning, supported by software tools, to analyse their designs. The idea is to build a mathematical model of a system and then try to prove properties of it that validate the system's correctness – or at least help discover subtle bugs. The proofs can be millions of lines long, so specially-designed computer algorithms are used to search for and check them.

This course provides a survey of several major software-assisted verification methods, covering both theory and practical applications. The aim is to familiarise students with the mathematical principles behind current verification technologies and give them an appreciation of how these technologies are used in industrial system design today.

Synopsis

  1. Introduction.
  2. Modelling sequential systems, Kripke structures.
  3. Temporal logic: LTL, CTL*, and CTL.
  4. Specifying systems with temporal logic.
  5. Reachability calculations, model checking.
  6. Binary Decision Diagrams (BDDs).
  7. Algorithms over BDDs.
  8. Combinational equivalence checking.
  9. Symbolic model checking.
  10. Propositional SAT.
  11. Model Checking with SAT.
  12. Abstraction Refinement.
  13. Decision procedures.
  14. Decision procedures in Model Checking.
  15. Practical, industrial-scale hardware verification.
  16. Computer-aided software verification.

Syllabus

Introduction to formal hardware verification. Binary Decision Diagrams and their use in combinational equivalence checking. Modelling sequential systems; Kripke structures. Specifying systems with temporal logic; CTL*, CTL and LTL. Reachability and symbolic model checking. New model checking approaches based on algorithms for Boolean satisfiability. Automatic abstraction refinement. Decision procedures and their use in combination with model checking. Practical, industrial-scale hardware verification. Current approaches to computer-aided software verification.

Reading list

The lectures will be supplemented with notes and pointers to published articles in the field. The following may be helpful for reference or further reading on specific topics.

Surveys

  • Formal Verification in Hardware Design: A Survey, by C. Kern and M. R. Greenstreet, ACM Transactions on Design Automation of Systems , vol. 4 (April 1999), pp. 123-193.
  • A Survey of Automated Techniques for Formal Software Verification , by D'Silva et al., IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2008
Temporal Logic and Model Checking
Binary Decision Diagrams and SAT
BDDs and Model Checking
  • Logic in Computer Science: Modelling and reasoning about systems, by Michael Huth and Mark Ryan (Cambridge University Press, 2000).
  • Model Checking, by Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, Second printing (The MIT Press, 2000).
  • Concepts, Algorithms, and Tools for Model Checking, Unpublished lecture notes by J.-P. Katoen, 1998.

Related research

Themes

Activities

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.