Syllabus for CS357: Techniques for Program Analysis and Verification


Lectures are in room 200-219 in the History corner, TuTH, 9:30-10:45.

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. Students will do homeworks and a final project.

Assignment 1 is due Tuesday, Oct. 25

Assignment 2 is due Tuesday, Nov. 8
Assignment 2 solutions

Assignment 3 is due Monday, Dec. 12

Date Lecture Speaker Topic Reading Assigned Due
9/27 Tuesday 1 Aiken Overview
9/29 Thursday 2 Dill Boolean Satisfiability [SS99][MMZZM01]
10/4 Tuesday 3 Aiken Program Analysis in Saturn [ISSTA00] [TACAS04] [POPL05]
10/6 Thursday 4 Dill Bit Vectors and Arrays [GD07]
10/11 Tuesday 5 Dill Boolean Decision Diagrams (BDDs) [B86] [BBR90] [R93]
10/13 Thursday 6 Dill Model Checking and Temporal Logic [CES86]
10/18 Tuesday 7 Dill Symbolic Model Checking with BDDs [BCLMD94] [BCMDH92]
10/20 Thursday 8 Dill Symbolic Model Checking II [CM90]
10/25 Tuesday 9 Aiken Simplifying Boolean Formulas [DDA]
10/27 Thursday 10 Dill BDD's for program analysis [WL04] [W06]
11/1 Thursday 11 Dill Counter-Example Guided Abstraction Refinement [DDP99][DD02]
11/3 Thursday 12 Dill CEGAR, cont
11/8 Thursday 13 Dill Interpolation [M03] [MJ06]
11/10 Thursday 14 Aiken Over and Underapproximations [PLDI08] [ESOP10]
11/15 Tuesday 15 Aiken Integer Constraints [CACM92] [CAV09]
11/17 Thursday 16 Aiken Set Constraints [CSL93]
11/29 Tuesday 17 Aiken Cubic-time Set Constraints [PLDI98] [PLDI88] [OOPSLA91] [Andersen94, Chapter 4]
12/1 Thursday 18 Aiken Abstract Interpretation [JACM76] [POPL77]
12/6 Tuesday 19 Aiken Type-Based Analysis [LISP&FP92] [POPL96] [Survey91] [ESOP01]
12/8 Thursday 20 Aiken Context Sensitivity [POPL95] [PEPM97] [TOPLAS00] [PLDI04] [PLDI06] [PLDI07]