Course Description
This course covers both foundations and practical aspects of the automated analysis of programs, which is becoming increasingly critical to find software errors and assure program correctness. The theory of abstract interpretation captures the essence of a broad range of program analyses and supports reasoning about their correctness. Building on this foundation, the course will describe program representations, data flow analysis, alias analysis, interprocedural analysis, dynamic analysis, and symbolic execution. Through assignments and projects, students will design and implement practical analysis tools that find bugs and verify properties of software.
This course fulfills the Logic and Languages constrained elective category for the Computer Science major as well as the Theoretical Foundations requirement of the Computer Science master's degree.
Why take this course?
- Explore the meaning of programs. One of the most basic questions that programmers ask is "What does this program do?" Program analysis is all about understanding programs--automatically!
- Learn deep theory. The theory of abstract interpretation stands with type theory as the most important and beautiful foundations of programming languages. Abstract interpretation is the fundamental theory of abstraction: how to precisely relate the concrete execution of a program to an abstraction of that execution. Naturally, this has many applications, which brings us to the third reason to take this course:
- Build awesome tools. Using program analysis, you can build tools that find bugs, prove important security and correctness properties, automatically generate useful tests, and much more--and you'll have a chance to do all of this in course assignments and a project that you can design yourself (if you want).
Logistics and People
Class: Tue/Thu 11:00 a.m. — 12:20 p.m. in WEH 2302
Recitation: Fri 10:00 a.m. — 10:50 a.m. in BH A51
Spring 2023
12 units
Course Syllabus and Policies
The syllabus covers course learning objectives, supplemental textbooks, assessments, late work policy, and policies. Consult Canvas and especially Piazza for up-to-date announcements and discussion (links in header).
Schedule
As of January 2023, we have endeavored to make this schedule, including assignment due dates, as accurate as possible. However, it is subject to change as the semester advances.
| Date | Topic | Reading/Material | HW Due | Optional Reading | |
|---|---|---|---|---|---|
| Jan 17 | Introduction, Program Representation, and Syntactic Analysis | Text ch. 1 & 2 slides | PPA ch. 1 | ||
| Jan 19 | Program Semantics | Text ch. 3 slides | |||
| Jan 20 | recitation CodeQL | notes | |||
| Jan 24 | Program Semantics (con) | ||||
| Jan 26 | Dataflow Analysis & Abstract Interpretation Framework | Text ch. 4 | hw1 (see Canvas) | PPA ch. 2 & 6 | |
| Jan 27 | recitation Semantics | notes, solutions | |||
| Jan 31 | Dataflow Analysis examples | Text ch. 5 | PPA ch. 2.1 | ||
| Feb 2 | Dataflow Analysis examples (con) | hw2 pdf mathpartir | PPA ch. 2 | ||
| Feb 3 | recitation Specifying/Implementing Dataflow Analysis | (see hw3) | |||
| Feb 7 | Dataflow Analysis examples (Con), Termination and Complexity | Text ch. 6 | PPA ch. 2.2—2.3 | ||
| Feb 9 | Dataflow Analysis: Termination and Complexity | hw3 pdf | PPA ch. 2.3—2.4 | ||
| Feb 10 | recitation Data-Flow Analysis Correctness | notes, solutions | |||
| Feb 14 | Widening and Collecting | Text ch. 7 | PPA ch. 2.5 | ||
| Feb 16 | Interprocedural analysis | Text ch. 8 | hw4 pdf | PPA ch. 2.5 | |
| Feb 17 | recitation | repo | |||
| Feb 21 | Context-Sensitive Analysis | Text ch. 8 & ch. 10.2 | |||
| Feb 23 | Pointer Analysis + Call Graphs for Object-Oriented Languages | Text ch. 10 | |||
| Feb 24 | recitation Midterm review | Midterm Study Guide | |||
| Feb 28 | Midterm exam 1 | midterm | |||
| Mar 2 | Control-Flow Analysis for Functional Languages | Text ch. 9 | hw5 checkpoint pdf | PPA ch. 3 | |
| Mar 3 | no recitation | ||||
| Mar 6—10 | Spring Break; no classes | ||||
| Mar 14 | Intro to Hoare Logic | Text ch. 11 | |||
| Mar 16 | Verification using Hoare Logic | Text ch. 11 | hw5 pdf | ||
| Mar 17 | recitation Hoare Logic Proofs using Axiomatic Semantics | notes, solutions | |||
| Mar 21 | Symbolic Execution | Text ch. 13 | |||
| Mar 23 | Satisfiability Modulo Theories | Text ch. 12 | |||
| Mar 24 | recitation Intro to Z3 | repo | |||
| Mar 28 | Concolic Testing | Text ch. 14 | hw6 pdf | ||
| Mar 30 | Program Synthesis | Text ch. 15 | |||
| Mar 31 | recitation Simple synthesis using Z3 | repo | |||
| Apr 4 | Program Synthesis (2/2), Program Repair | hw7pdf project proposal |
|||
| Apr 6 | Program Repair | CACM overview paper, slides | |||
| Apr 7 | Midterm review | ||||
| Apr 11 | Dynamic Analysis (Fuzz Testing, Invariant Generation) | Text ch. 16 | hw8pdf |
||
| Apr 13 | Spring carnival; no class | ||||
| Apr 14 | No recitation | ||||
| Apr 18 | Dynamic Race Detection | slides | |||
| Apr 20 | Midterm exam 2 | midterm | |||
| Apr | recitation Dynamic analysis on stack machine bytecode | repo | |||
| Apr 25 | TBA | ||||
| Apr 27 | Review | project checkpoint |
|||
| Apr 28 | recitation Project Discussions | ||||
| May 8, 1--4 pm | Project Presentations | ||||
| May 8 (midnight) | project final report |