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 TBD
Office DC2522  
email first . last AT first . last AT



Week Lecture Reading
1 Admin
Model Checking
E.M. Clarke. The Birth of Model Checking
The Model Checking Handbook
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)
5 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
6 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
7 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 and CHC-LRA Bjorner et al. Horn Clause Solvers for Program Verification
10 LIA and ICE Ch. 6.4 (logical view) and 6.7 in Understanding and Using Linear Programming
A. Gurfinkel. IC3, PDR, and Friends
(New) P. Garg et al. ICE: a robust framework for learning invariants
(New) Y. Vizel et al. IC3 - Flipping the E in ICE

Important Dates (likely to change, check frequently)

Sep 7 A1 out
Sep 28 No class
Oct 5 A1 due
Oct 5 A2 out
Oct 12 Class at usual time and place
Nov 2 A2 due
Nov 2 A3 out
Nov 02 Project proposal due
Nov 02 No class
Nov 30 A3 due
Nov 30 last class
Dec 15 Project presentations