Lecturer	Tom Melham
Class Tutor	Daniel Kroening
Class Exercise Marker	Peter Boehm
Degrees	Schedule C1 — Computer Science Part C — Mathematics and Computer Science Schedule C — MSc in Advanced Computer Science MSc by Research MSc in Mathematics and Foundations of Computer Science
Term	Michaelmas Term 2008  (20 lectures)

Overview

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 an in-depth 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. The application focus is on formal verification of hardware designs, currently the most successful application of computer-aided verification. The course does not, however, require advanced background knowledge of digital logic or hardware design.

Synopsis

1. Introduction to formal hardware verification.
2. Binary Decision Diagrams (BDDs)
3. Algorithms over BDDs.
4. Combinational equivalence checking.
5. Modelling sequential systems, Kripke structures.
6. Temporal logic: CTL*, CTL and LTL.
7. Specifying systems with temporal logic.
8. Reachability calculations, model checking.
9. Symbolic model checking.
10. SAT-based verification.
11. Symbolic trajectory evaluation.
12. A verification methodology.
13. Deductive theorem proving.
14. Hybrid approaches.
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. Symbolic trajectory evaluation and abstraction. Deductive theorem proving and its 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 of Hardware Verification

• Introduction to Formal Hardware Verification, by Thomas Kropf (Spinger-Verlag, 1998).
• `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.
• Formal Hardware Verification : Methods and Systems in Comparison, edited by Thomas Kropf, Lecture Notes in Computer Science, vol. 1287 (Springer-Verlag, 1997).

Binary Decision Diagrams

• An Introduction to Binary Decision Diagrams, by Henrik Reif Andersen, Lecture Notes (Technical University of Denmark, October 1997). [PDF]
• `Formal Hardware Verification with BDDs: An Introduction', by Alan J. Hu, IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (1997), pp. 677-682.

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.

Symbolic Trajectory Evaluation

• `Formal verification by symbolic evaluation of partially-ordered trajectories', by C.-J. H. Seger and R. E. Bryant, Formal Methods in System Design, vol. 6 (1995), pp. 147-189.
• `Practical Formal Verification in Microprocessor Design', by R. B. Jones, J. W. O'Leary, C.-J. H. Seger, M. D. Aagaard, and T. F. Melham, IEEE Design & Test of Computers, vol. 18, no. 4 (July/August 2001), pp. 16-25.

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.