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 2:00 p.m. — 3:20 p.m. in
WEH 5328
Recitation: Fri 10:00 a.m. — 10:50 a.m. in
WEH 5320
Fall 2026
12 units
Office hours (Effective Sep. 21):
Tuesdays 3:30 p.m. — 4:30 p.m.
Wednesdays 2:00 p.m. — 3:00 p.m.
Location: TCS 360
Email: yiliangl@andrew.cmu.edu
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
We are still working to finalize the schedule for Fall 2026. The schedule below is a draft and is subject to significant change.
| Date | Topic | Reading/Material | HW Due | Optional Reading | |
|---|---|---|---|---|---|
| Aug 25 | Introduction, Program Representation, and Syntactic Analysis | Text ch. 1 & 2 | PPA ch. 1 | ||
| Aug 27 | Program Semantics | Text ch. 3 | |||
| Aug 28 | recitation CodeQL | repo sol-ex1 sol-ex2 | |||
| Sep 1 | Program Semantics (cont.) | ||||
| Sep 3 | Program Semantics (cont.) | hw1 repo | PPA ch. 2 & 6 | ||
| Sep 4 | recitation Semantics | slides problems solutions | |||
| Sep 8 | Program Semantics (cont.) | ||||
| Sep 10 | Dataflow Analysis & Abstract Interpretation Framework | Text ch. 4 | PPA ch. 2.1 | ||
| Sep 11 | recitation HW3 setup | ||||
| Sep 15 | Dataflow Analysis examples (cont.) |
hw2 (now due Tue.) pdf tex mathpartir |
PPA ch. 2.2—2.3 | ||
| Sep 17 | Termination and Correctness | Text ch. 6 | PPA ch. 2.3—2.4 | ||
| Sep 18 | recitation Data-Flow Analysis Correctness | problems solutions | |||
| Sep 22 | Termination and Correctness |
hw3 (now due Tue.) pdf repo |
PPA ch. 2.5 | ||
| Sep 24 | Termination and Precision | Text ch. 7 | PPA ch. 2.5 | ||
| Sep 25 | recitation Dataflow analysis using Soot | repo solutions | |||
| Sep 29 | Interprocedural analysis | Text ch. 8 |
hw4 (now due Tue.) pdf tex |
||
| Oct 1 | Context-Sensitive Analysis / Interprocedural Analysis | Text ch. 8 & ch. 10.2 | |||
| Oct 2 | recitation Midterm review |
study guide (sp25)
study guide (fa24) |
|||
| Oct 6 | Widening and Collecting Operators | Text ch. 10 |
hw5 checkpoint pdf repo |
PPA ch. 3 | |
| Oct 8 | Midterm exam 1 | midterm | |||
| Oct 9 | no recitation | ||||
| Oct 12-16 | Fall Break; no classes | ||||
| Oct 20 | Axiomatic Semantics + Hoare Logic | Text ch. 11 | |||
| Oct 22 | Hoare Logic + Verification | Text ch. 11 | |||
| Oct 23 | recitation Hoare Logic Proofs + Midterm 1 Recap | problems solutions | |||
| Oct 26 |
hw5 (now due Mon.) pdf repo |
||||
| Oct 27 | Verification + Pointer Analysis + SAT/SMT | Text ch. 10.1, 12 | |||
| Oct 29 | SAT/SMT | Text ch. 12 | |||
| Oct 30 | recitation Midterm 1 Recap + Intro to Z3 | repo sol | hw6 pdf tex | ||
| Nov 3 | Democracy Day; no class | ||||
| Nov 5 | SAT/SMT | Text ch. 12, 15 | |||
| Nov 6 | recitation Simple synthesis using Z3 | repo ex1-sol ex2-sol | |||
| Nov 10 | Bug-Finding | Text ch. 13, 14, 16 | project proposal spec | ||
| Nov 12 | Theorem Proving | ||||
| Nov 13 | recitation TBD | ||||
| Nov 17 | Theorem Proving | ||||
| Nov 19 | Lightweight Formal Modeling (Alloy) |
CACM article
tool |
hw7 Q1,2 pdf tex | ||
| Nov 20 | recitation Midterm 2 review | ||||
| Nov 24 | Midterm exam 2 | midterm | |||
| Nov 26 | Thanksgiving Break; no class | ||||
| Nov 27 | No recitation | ||||
| Dec 1 |
Guest Lectures (Deian Stefan): Information Flow Control |
project checkpoint
spec
hw7 q3 paper selection (optional bonus) |
|||
| Dec 3 | Review and Project Discussions | ||||
| Dec 4 | recitation Bug-Finding Paper Presentations | hw7 q3 paper presentation (optional bonus) | |||
| Dec 11 | Project Presentations (5:30-8:30pm) |
project final report |