ComputerAided Formal Verification: 20122013
Lecturer 

Degrees 
Schedule B2 — Computer Science 
Term 
Michaelmas Term 2012 (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 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 speciallydesigned computer algorithms are used to search for and check them.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 give them an appreciation of how these technologies are used in industrial system design today.
Synopsis
 Introduction.
 Modelling sequential systems, Kripke structures.
 Temporal logic: LTL, CTL*, and CTL.
 Specifying systems with temporal logic.
 Reachability calculations, model checking.
 Binary Decision Diagrams (BDDs).
 Algorithms over BDDs.
 Combinational equivalence checking.
 Symbolic model checking.
 Propositional SAT.
 Model Checking with SAT.
 Abstraction Refinement.
 Decision procedures.
 Decision procedures in Model Checking.
 Practical, industrialscale hardware verification.
 Computeraided 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, industrialscale hardware verification. Current approaches to computeraided 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. 123193.
 A Survey of Automated Techniques for Formal Software Verification , by D'Silva et al., IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems (TCAD), 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 (1997), pp. 677682.
 Chapter 2 in Decision Procedures, by Daniel Kroening and Ofer Strichman, Springer, 2008
 Handbook of Satisfiability, Biere, Heule, Van Maaren, Walsh, IOS Press 2009
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 at the Department of Computer Science
Themes 

Activities 