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 | |
| first . last AT uwaterloo.ca | first . last AT uwaterloo.ca |
| 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 |