The course will focus on SAT and SMT technology and their applications. The students will learn the theoretical foundations of SAT/SMT, how to use SAT/SMT technology to solve problems, and finally how to implement a small theory solver of their own. The course will build up towards various applications of SAT/SMT technology in the context of verification.
Students are expected to do the assigned readings, attend the lectures and participate in class discussion. There will be 3 homeworks and a final group project.
None; research papers will be assigned as weekly reading.
There will be 3 assignments throughout the course, gradually leading the students from using to implementing (some elements) of the SAT/SMT technology.
Assignment 1 - Deadline October 20th
Assignment 2 - Deadline November 7th — Solution
Assignment 3 - Deadline November 26th December 1st
Project proposals ~ Send an email to indicate interest by Monday November 11. Include a project proposal or indicate interest in one of the stock projects (CDCL SAT solver, Bounded-Model Checker).
Project reports due by December 15th, this deadline is STRICT.
If you are rotating with the lab I need only a write up of your project with the lab.
Your report should contain:
Piazza will be the primary form of communication about the course. Office hours can be arranged via email.
https://piazza.com/stanford/fall2019/cs357/home
Tuesdays and Thursdays: 10:30 AM - 11:50 AM at 420-050(Jordan Hall) between 09/23/2019 - 12/06/2019
Week | Date | Topic | Reading |
---|---|---|---|
1 | 9/22 | Introduction | |
1 | 9/24 | Propositional logic - part 1 | (optional) Enderton's - A Mathematical Introduction to Logic, Ch. 1 |
2 | 10/01 | Propositional logic - part 2 | |
2 | 10/03 | DP, DPLL | DP60, DPLL62 |
3 | 10/08 | Abstract DPLL, CDCL | NOT04 Sec. 1-2, SS99, MMZZM01 |
3 | 10/10 | Abstract DPLL, CDCL | For State of the Art see Armin Biere's slides at SAT/SMT Summer School |
4 | 10/15 | First Order Logic | (optional) Enderton's - A Mathematical Introduction to Logic, Ch. 2, Sec. 1-3 |
4 | 10/17 | Deduction in FOL | (optional) Enderton's - A Mathematical Introduction to Logic, Ch. 2, Sec. 4- |
5 | 10/22 | Intro to SMT | |
5 | 10/24 | From Sat to SMT | NOT04 |
6 | 10/29 | Nelson-Oppen | (reading list at the end of slides) |
6 | 10/31 | Model Checking (by Makai Mann) | (see MC resources below) |
7 | 11/05 | Homework discussion, Congruence Closure | |
7 | 11/07 | Simplex, Bit-Vectors | See Intro to SMT by D. Jovanovic and Decision Procedures Bit-vectors material |
8 | 11/12 | SyGuS, Assignment 3 overview | |
8 | 11/14 | CANCELLED | |
9 | 11/19 | Proofs in SAT | RAT, Extended Resolution Simulates DRAT, LRAT, Proofs in SMT |
9 | 11/21 | IC3 (by Makai Mann) | |
10 | 12/02 | Overview of Hoare Calculus, CEGAR, Abstract interpretation | Hoare69, CEGAR, Abstract Interpretation in a Nutshell |
BDD-based Model Checking — Symbolic Model Checking: 10^20 States and Beyond (1990)
Bounded Model Checking — Symbolic Model Checking without BDDs (1999)
K-Induction — Checking safety properties using induction and a SAT-solver (2000)
Liveness to Safety — Liveness Checking as Safety Checking (2002)
Interpolation Based Model Checking — Interpolation and SAT-based Model Checking (2003)
Survey on Hardware Verification — A Survey of Recent Advances in SAT-Based Formal Verification (2005)
Property Directed Reachability (PDR/IC3) — SAT-Based Model Checking without Unrolling (2011), Understanding IC3 (2012)
Lectures: Aleksandar Zeljić (zeljic [at] stanford [dot] edu)
TA: Makai Mann