Course Description

Computer systems are becoming smaller, faster, pervasive, ubiquitous, mobile, connected, adaptable, and “smart”. We are increasingly becoming more dependent on their correct operation. The border between safety-critical and non-safety-critical systems is being eroded. Dealing with complexity requires increased automation in development, testing, verification, and certification.

The dream of a mechanical verifier is as old as Computer Science itself. However, only in the last few decades have we seen a major breakthrough towards making it a reality. Starting with the adoption of Model Checking (a.k.a, Formal Verification) by the hardware semiconductor industry in the mid 90s, new techniques have emerged that combine decision procedures with novel heuristics to significantly automate software verification, testing, and certification.

The course will introduce students to the state-of-the-art research in automated verification. The course focuses on the recent advances in SAT and SMT-based automated verification techniques including: Conflict-Driven Clause-Learning (CDCL), Bounded Model Checking with SAT solvers, Unbounded Model Checking, Interpolation-based Model Checking, IC3, Property Directed Reachability (PDR), Software Model Checking, decision procedures for Constrained Horn Clauses, SMT-based Unbounded Model Checking, Predicate Abstraction, and Machine Learning-based Invariant Synthesis.

Additional information about the course is available in the course syllabus.

Details Instructor Teaching Assistant
Name Prof. Arie Gurfinkel None
Office DC2522  
email first . last AT uwaterloo.ca first . last AT uwaterloo.ca

Posts

Lectures

Week Lecture Reading
1 Admin
Model Checking
E.M. Clarke. The Birth of Model Checking
The Model Checking Handbook
Science, Art, and Magic of Constrained Horn Clauses
Spacer on Jupyter
2 SAT HBMC Ch. 9: Propositional SAT Solving
3 BMC HBMC Ch. 10: SAT-Based Model Checking
HBAR Ch. 14: Bounded Model Checking (upto Sec. 14.6)
D. Kroening et al. A Tool for Checking ANSI-C Programs
4 IND and SMC The k-induction Principle
Sheeran et al. Checking Safety Properties Using Induction and a SAT-Solver
Brayton and Mishchenko. Scalably-Verifiable Sequential Synthesis
(Optional) D. Kroening et al. Software Verification Using k-Induction

HBMC Ch. 7: Binary Decision Diagrams
HBMC Ch. 8: BDD-Based Symbolic Model Checking (upto Sec. 8.4.2)

Important Dates (likely to change, check frequently)

Sep 9 No class!!!
Sep 16 First lecture
Sep 16 A1 out
Oct 7 A2 out
Oct 11 A1 due
Nov 11 A3 out
Nov 15 A2 due
Nov 18 Project proposal due
Dec 02 A3 due
TBA Project presentations