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
(all times below in US Eastern Time; see Canvas for Zoom meeting links)
Class: Tue/Thu 10:10 a.m. — 11:30 a.m. in GHC 4101 or via Zoom (see schedule)
Recitation: Fri 10:10 a.m. — 11:00 a.m. via in MI 348 or via Zoom (see schedule)
Spring 2022
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 2022, 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 | Assignments Due | Modality | Optional Reading |
|---|---|---|---|---|---|
| Jan 18 | Introduction, Program Representation, and Syntactic Analysis | Text ch. 1 & 2, slides | Remote | PPA ch. 1 | |
| Jan 20 | Program Semantics | Text ch. 3, slides | Remote | ||
| Jan 21 | recitation CodeQL | notes | Remote | ||
| Jan 25 | Semantics (contd.) and Intro to Dataflow Analysis | Text ch. 3 & 4, slides (a) (b) | Remote | PPA ch. 2 | |
| Jan 27 | Dataflow Analysis & Abstract Interpretation Framework | Text ch. 4, slides | hw1 github | Remote | PPA ch. 2 & 6 |
| Jan 28 | recitation Semantics | notes, solutions | Remote | ||
| Feb 1 | Dataflow Analysis examples | Text ch. 5, slides | In-Person | PPA ch. 2.1 | |
| Feb 3 | Dataflow Analysis: Termination and Complexity | Text ch. 5, slides | hw2 pdf mathpartir | In-Person | PPA ch. 2 |
| Feb 4 | recitation Specifying/Implementing Dataflow Analysis | (see hw3) | Remote | ||
| Feb 8 | Dataflow Analysis: Soundness | Text ch. 6, slides | In-Person | PPA ch. 2.2—2.3 | |
| Feb 10 | Dataflow Analysis: Precision | Text ch. 6, same slides | hw3 pdf | In-Person | PPA ch. 2.3—2.4 |
| Feb 11 | recitation Data-Flow Analysis Correctness | notes, solutions | In-Person | ||
| Feb 15 | Interprocedural analysis | Text ch. 8, slides handout 1, handout 2 |
In-Person | PPA ch. 2.5 | |
| Feb 17 | Context-Sensitive Analysis | Text ch. 8 slides | hw4 pdf | In-Person | PPA ch. 2.5 |
| Feb 18 | recitation | repo | In-Person | ||
| Feb 22 | Pointer Analysis + Call Graphs for Object-Oriented Languages | Text ch. 10, slides | In-Person | ||
| Feb 24 | Pointer Analysis (contd.) | Text ch. 10, same slides | hw5 checkpoint pdf | In-Person | |
| Feb 25 | recitation Midterm review | Midterm Study Guide | In-Person | ||
| Mar 1 | Mid-term exam | midterm | In-Person + Take-home |
||
| Mar 3 | Control-Flow Analysis for Functional Languages | Text ch. 9, slides, handout | hw5 pdf | In-Person | PPA ch. 3 |
| Mar 4 | no recitation | ||||
| Mar 7—11 | Spring Break; no classes | ||||
| Mar 15 | Intro to Hoare Logic | Text ch. 11, slides | In-Person | ||
| Mar 17 | Verification using Hoare Logic | Text ch. 11, same slides | In-Person | ||
| Mar 18 | recitation Hoare Logic Proofs using Axiomatic Semantics | notes, solutions | In-Person | ||
| Mar 22 | Symbolic Execution | Text ch. 13, slides | In-Person | ||
| Mar 24 | Satisfiability Modulo Theories | Text ch. 12, slides | In-Person | ||
| Mar 25 | recitation Intro to Z3 | repo | In-Person | ||
| Mar 29 | Concolic Testing | Text ch. 14, slides | hw6 pdf | In-Person | |
| Mar 31 | Program Synthesis | Text ch. 15, slides | In-Person | ||
| Apr 1 | recitation Simple synthesis using Z3 | repo | In-Person | ||
| Apr 5 | Fuzz Testing | Text ch. 16, slides | hw7 pdf | In-Person | |
| Apr 7 | Spring carnival; no class | In-Person | |||
| Apr 8 | no recitation | ||||
| Apr 12 | Automatic Program Repair | slides, GenProg paper | In-Person | ||
| Apr 14 | Dynamic Analysis (+ Invariant Generation) | slides, Daikon paper | hw8 pdf (project handout) |
In-Person | |
| Apr 16 | recitation Dynamic analysis on stack machine bytecode | repo | In-Person | ||
| Apr 19 | Dynamic Race Detection - I | slides | Remote | ||
| Apr 21 | Dynamic Race Detection - II | same slides | Remote | ||
| Apr 22 | recitation Project Discussions | Remote | |||
| Apr 26 | Guest Lecture: Fraser Brown | Remote | |||
| Apr 28 | Review | slides | project checkpoint same pdf |
Hybrid? | |
| Apr 29 | recitation Project Discussions | Remote | |||
| May 9 (1-4pm) | Project Presentations | In-Person (GHC 4307) |
|||
| May 9 (midnight) | project final report same pdf |