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.
|Name||Prof. Arie Gurfinkel||None|
|first . last AT uwaterloo.ca||first . last AT uwaterloo.ca|
|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)
|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|