CS357: Techniques for Program Analysis and Verification

Program analysis and formal verification are similar research areas with largely separate research communities, mostly for historical reasons. However, a lot of the most creative recent work in both areas has resulted from ideas and techniques from one field being imported into the other.

This course is intended to promote that cross-fertilization by covering major ideas from each field that may be broadly useful. We expect it will be of interest to students working on program analysis, verification, and other areas where these techniques may be applicable -- but not yet widely applied. The emphasis will be on methods that are applicable in practice, although the underlying theory will also be taught.

In addition to lectures by Profs. Aiken and Dill, there will be several guest lectures by Prof. Clark Barrett of NYU, who is a leading expert on SMT solvers.

Location Room 320-106 in the Braun Corner, MW 1:30-2:50
Prerequisites Undergraduate CS theory (particularly basic logic); knowledge of compilers will also be helpful
Textbook None; lecture notes and research papers assigned as readings will be posted here
Communication Class mailing list (for occasional announcements)
Piazza (for questions and discussion)
E-mail (see staff list below)
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.
E-mail Office Office hours
Alex Aiken (Instructor) aiken@cs.stanford.edu Gates 411 Tue 3-4 (except 9/29) and by appointment
David Dill (Instructor) dill@cs.stanford.edu Gates 344 by appointment
Clark Barrett (Instructor) barrett@cs.nyu.edu Gates 343 by appointment
Stefan Heule (TA) sheule@cs.stanford.edu Gates 420 Wed 10-12, and by appointment
Assigned Due
Assignment #1 10/5 10/19
Assignment #2 10/19 11/2
Project proposal 11/9
Assignment #3 11/2 11/16
Project presentation & demo 12/9, 2-4pm, Gates 498
Project code submission 12/10

Date Lecture Speaker Topic Reading
9/21 Monday 1 Aiken Overview
9/23 Wednesday 2 Dill Boolean Satisfiability [SS99] [MMZZM01]
9/28 Monday 3 Aiken Program Analysis in Saturn [ISSTA00] [TACAS04] [POPL05]
9/30 Wednesday 4 Dill Boolean Satisfiability (continued)
10/5 Monday 5 Dill Boolean Decision Diagrams (BDDs) [B86] [BBR90] [R93]
10/7 Wednesday 6 Dill Model Checking and Temporal Logic [CES86]
10/12 Monday 7 Dill Symbolic Model Checking with BDDs (same slides as previous lecture) [BCLMD94] [BCMDH92] [CM90]
10/14 Wednesday 8 Dill Symbolic Model Checking with BDDs (same slides as previous lecture)
10/19 Monday 9 Barrett From SAT to SMT [BSST09], Sections 12.1, 12.2, and 12.4.
10/21 Wednesday 10 Barrett Theory Solvers in SMT [WBW16] [BT15], Sections 3 and 4
10/26 Monday 11 Aiken Loop Invariants [SA14] [ECGN00]
10/28 Wednesday 12 Aiken Program Equivalence [SSA13] [SSCA13] [SSCA15]
11/2 Monday 13 Barrett Theory Combination and New Insights on the Nelson-Oppen Combination Method [JB10] [JB13]
11/4 Wednesday 14 Barrett Solving Arithmetic Constraints [KBD13] [KBT14]
11/9 Monday 15 Aiken Over- and Underapproximations in Program Analysis [PLDI08] [ESOP10]
11/11 Wednesday 16 Aiken Abstract Interpretation [JACM76] [POPL77]
11/16 Monday 17 Clark Lazy and Eager Approaches to Bit-Vector Solving and STP: A Decision Procedure for Bit-Vectors and Arrays [GD07] [HBJ+14]
11/18 Wednesday 18 Dill Symbolic model checking without BDDs
11/30 Monday 19 Aiken Abstract Interpretation (Part 2)
12/2 Wednesday 20 Dill