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.
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.
Tuesdays and Thursdays: 10:30 AM - 11:50 AM at 420-050(Jordan Hall) between 09/23/2019 - 12/06/2019
|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|
|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)
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)
Lectures: Aleksandar Zeljić (zeljic [at] stanford [dot] edu)
TA: Makai Mann