Lecturer	David Parker
Degrees	Schedule A2(CS&P) — Computer Science and Philosophy Schedule B1 (CS&P) — Computer Science and Philosophy Schedule A2 — Computer Science Schedule B1 — Computer Science Schedule A2(M&CS) — Mathematics and Computer Science Schedule B1(M&CS) — Mathematics and Computer Science Michaelmas Term — MSc in Advanced Computer Science
Term	Michaelmas Term 2024  (16 lectures)

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 automated software tools, to analyse their designs. The idea is to build a mathematical model of a system and then try to prove formal properties of it that validate the system's correctness, or at least that 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. Properties are formalised as formulae in proper temporal logics.

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 provide them with an appreciation of how these technologies are used in industrial system design today.

Synopsis

• Introduction to CAFV 
• Modelling sequential and parallel systems
• Linear-time properties 
• Linear temporal logic (LTL) 
• Computation tree logic (CTL) and CTL*  
• Counterexamples and witnesses 
• Model checking CTL
• Model checking LTL
• Binary decision diagrams (BDDs)
• Symbolic model checking 
• Model checking with SAT, bounded model checking 
• Completeness thresholds and k-induction
• Symbolic execution
• Craig interpolation 
• Equivalences and abstractions 
• Hardware verification
• Practical, industrial-scale verification; present challenges 

Syllabus

Introduction to computer-aided formal verification. Modelling sequential and parallel systems as labelled transition systems. Linear time properties. Temporal logics: linear temporal logic (LTL), computation tree logic (CTL) and CTL*. Model checking CTLand LTL. Counterexamples and witnesses. Symbolic model checking. Bounded model checking via SAT. Symbolic execution. Craig interpolation. Equivalences and abstractions. Hardware verification. Practical, industrial-scale verification; present challenges 

Reading list

The lecture slides will act as course notes. For the first half of the course (on model checking), we will closely follow parts of this textbook, which is recommended reading:

• Principles of Model Checking, by C. Baier and J.-P. Katoen (The MIT Press, 2008)

Other useful references on model checking are:

• 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 edition (The MIT Press, 2000)

The above will be supplemented with notes and pointers to published articles in the field, which may be helpful for reference or further reading on specific topics. Examples include:

Surveys:

• Formal Verification in Hardware Design: A Survey, by C. Kern and M. R. Greenstreet, ACM Transactions on Design Automation of Systems, v. 4, pp. 123-193, 2009
• 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, v. 27(7), pp. 1165-1178, 2008

Binary Decision Diagrams and SAT:

• An Introduction to Binary Decision Diagrams, by Henrik Reif Andersen, Lecture Notes (Technical University of Denmark, October 1997) 
• Formal Hardware Verification with BDDs: An Introduction, by Alan J. Hu, IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing, pp. 677-682, 1997  
• Decision Procedures, by Daniel Kroening and Ofer Strichman (Springer Verlag, 2008)

Related research

Themes	Automated Verification
Activities	Model Checking | Concurrency | Software Model Checking | Hardware Verification | Quantitative Analysis and Verification | Verification

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.