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 BMC Encodings  
- Reading Week  
5 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)
6 IMC and ITP HBAR Ch. 14: Bounded Model Checking (from Sec. 14.6)
K.L. McMillan. Interpolation and SAT-Based Model Checking
Y. Vizel and O. Grumberg. Interpolation-Sequence Based Model Checking
A. Gurfinkel and Y. Vizel. DRUPing for Interpolants
(Optional) HBMC Ch. 14: Interpolation and Model Checking
7 IC3 and PDR A. Bradley. SAT-based Model Checking without Unrolling
N. Eén, A. Mishchenko, R. K. Brayton. Efficient implementation of property directed reachability
A. Gurfinkel and A. Ivrii. Pushing to the Top
A. Bradley. Understanding IC3
HBMC Ch. 20: Model Checking and Deduction
7b IC3 and PDR  
8 FOL, SMT HBMC Ch. 11: Satisfiability Modulo Theories
Cimatti et al. IC3 Modulo Theories via Implicit Predicate Abstraction
Gurfinkel et al. Efficient Predicate Abstraction of Program Summaries
HBMC Ch. 20: Model Checking and Deduction
9 CHC
(Old) CHC and LIA
(Old) ICE
A. Gurfinkel and J. Navas. Automatic Program Verification with Seahorn
A. Gurfinkel. IC3, PDR, and Friends
Bjorner et al. Horn Clause Solvers for Program Verification

Important Dates (likely to change, check frequently)

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