CS 357 Advanced Topics in Formal Methods

Course description:

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.

Requirements:

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.

Textbook:

None; research papers will be assigned as weekly reading.

Assignments and Project

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

Assignment 3 - Deadline November 26th

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

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

Schedule

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 Applications - SyGuS, Assignment 3 overview
8 11/14 CANCELLED
9 11/19 Proofs in SAT/SMT
9 11/21 IC3
10 12/02 Abstract interpretation, Approximation Frameworks
Additional resources
MC Resources

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)

People

Lectures: Aleksandar Zeljić (zeljic [at] stanford [dot] edu)

TA: Makai Mann