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).
Projects due ~ Week 10/11 (flexible)
Students rotating with the lab can waive project work with the rotation.
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||Applications - SyGuS, Assignment 3 overview|
|9||11/19||Proofs in SAT/SMT|
|10||12/02||Abstract interpretation, Approximation Frameworks|
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