ComputerAided Formal Verification: 20172018
Lecturer 

Degrees 
Schedule S1(CS&P) — Computer Science and Philosophy Schedule B2 (CS&P) — Computer Science and Philosophy Schedule S1 — Computer Science Schedule B2 — Computer Science Schedule S1(M&CS) — Mathematics and Computer Science Schedule B2 — Mathematics and Computer Science 
Term 
Michaelmas Term 2017 (16 lectures) 
Overview
This course introduces the fundamentals of computeraided formal verification. Computeraided 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 speciallydesigned 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 softwareassisted 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 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 kinduction
 Craig interpolation
 Equivalences and abstractions
 Decision procedures in model checking
 Practical, industrialscale verification; present challenges
Syllabus
Introduction to computeraided 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 kinduction. Craig interpolation. Equivalences and abstractions. Decision procedures in model checking. Practical, industrialscale 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.
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. 123193, 2009
 A Survey of Automated Techniques for Formal Software Verification, by D'Silva et al., IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, v. 27(7), pp. 11651178, 2008
 From Philosophical to Industrial Logics, by M. Vardi, ICLA 2009
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. 677682, 1997
 Decision Procedures, by Daniel Kroening and Ofer Strichman (Springer Verlag, 2008)
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 at the Department of Computer Science
Themes 

Activities 
Verification  Quantitative Analysis and Verification  Hardware Verification  Software Model Checking  Concurrency  Model Checking 