Skip to main content

Computer-Aided Formal Verification:  2019-2020



Schedule S1(CS&P)(3rd years)Computer Science and Philosophy

Schedule S1(3rd years)Computer Science

Schedule S1(M&CS)(3rd years)Mathematics and Computer Science

Schedule BMSc in Advanced Computer Science

MSc in Mathematics and Foundations of Computer Science



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.


  1. Introduction to CAFV 
  2. Modelling sequential systems as labelled transition systems (Kripke structures)
  3. Linear time properties 
  4. Linear temporal logic (LTL) 
  5. Computation tree logic (CTL) and CTL*  
  6. Counterexamples and witnesses 
  7. Model checking CTL
  8. Model checking LTL
  9. Binary decision diagrams (BDD) 
  10. Symbolic model checking 
  11. Model checking with SAT, bounded model checking 
  12. Completeness thresholds and k-induction 
  13. Craig interpolation 
  14. Equivalences and abstractions 
  15. Decision procedures in model checking 
  16. Practical, industrial-scale verification; present challenges 


Introduction to computer-aided formal verification. Modelling sequential systems as labelled transition systems (Kripke structures). Linear time properties. Linear temporal logic (LTL). Computation tree logic (CTL) and CTL*. Model checking CTL. Model checking LTL. Counterexamples and witnesses. Binary decision diagrams (BDD). Symbolic model checking. Model checking with SAT, bounded model checking. Completeness thresholds and k-induction. Craig interpolation. Equivalences and abstractions. Decision procedures in model checking. Practical, industrial-scale verification; present challenges 

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.


Temporal Logics 

Binary Decision Diagrams and SAT

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 edition (The MIT Press, 2000) 
  • Principles of Model Checking, by C. Baier and J.-P. Katoen (The MIT Press, 2008)

Related research




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.