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

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

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:

  1. a description of what is the goal of the project and how it relates to the course (if not obvious)
  2. initial plan with proposal of evaluation
  3. a write up of what are the challenges you encountered along the way and how did you solve them.
  4. Results/evaluation, at least preliminary.
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  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
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)

SyGuS Resources

SyGuS

CEGIS

Divide and Conquer

CVC4SY

People

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

TA: Makai Mann