17-355/17-665/17-819 Program Analysis

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?

Logistics and People

Class: Tue/Thu 2:00 — 3:20 p.m. in GHC 4102
Recitation: Fri 10:00 a.m. — 10:50 a.m. in WEH 5320
Spring 2025
12 units

Professor Rohan Padhye
OH: Tu 3:30–4:30pm in TCS 325
Email: rohanpadhye@cmu.edu
Headshot of Professor Rohan Padhye
TA: Vasu Vikram
Office hours: Wed 3–4pm in TCS 310
Email: vasumv@cmu.edu
Headshot of teaching assistant Vasu Vikram

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 July 2025, 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
Aug 26 Introduction Text ch. 1 slides PPA ch. 1
Aug 28 Program Representations: Abstract Syntax and Operational Semantics Text ch. 2 & 3 slides
Aug 29 recitation CodeQL github
Sep 2 Program Semantics (cont.) Text ch. 2 & 3 same slides
Sep 4 Intermediate Representations, Control-Flow Graphs, and Data-Flow Text ch. 2 & 3 slides hw1 github PPA ch. 2 & 6
Sep 5 recitation Semantics notes soln
Sep 9 Dataflow Analysis & Abstract Interpretation Framework Text ch. 4, slides PPA ch. 2.1
Sep 11 Dataflow Analysis examples Text ch. 5 slides hw2 pdf mathpartir PPA ch. 2
Sep 12 recitation Specifying/Implementing Dataflow Analysis github
Sep 16 Data-Flow Analysis Algorithm: Termination, Complexity, and Fixed Point Text ch. 6, slides PPA ch. 2.2—2.3
Sep 18 Data-Flow Analysis: Soundness and Precision Text ch. 6, slides hw3 github PPA ch. 2.3—2.4
Sep 19 recitation Data-Flow Analysis Correctness notes soln
Sep 23 Interprocedural analysis: Introduction Text ch. 8 slides PPA ch. 2.5
Sep 25 Interprocedural analysis: Context-Sensitive Analysis Text ch. 8 slides
handout 1, handout 2
hw4 pdf PPA ch. 2.5
Sep 26 recitation
Sep 30 Pointer Analysis Text ch. 10 slides
Oct 2 Pointer Analysis (contd.) for Object-Oriented Languages same slides hw5 github
Oct 3 recitation Midterm 1 review. Midterm 1 Study Guide
Oct 7 Guest Lecture: Shrey Tiwari (Program Analysis Experience in Industry) PPA ch. 3
Oct 9 Midterm exam 1
Oct 10 no recitation
Oct 13—17 Fall Break; no classes
Oct 21 Intro to Hoare Logic Text ch. 11
Oct 23 Verification using Hoare Logic Text ch. 11
Oct 24 recitation Hoare Logic Proofs using Axiomatic Semantics
Oct 28 Symbolic Execution Text ch. 13
Oct 30 Concolic Testing Text ch. 14
Oct 31 recitation Intro to Z3
Nov 4 Democracy Day; no class
Nov 6 Dynamic Analysis (Fuzz Testing, Invariant Generation) Text ch. 16
Nov 7 recitation Dynamic analysis on stack machine bytecode
Nov 11 Satisfiability Modulo Theories Text ch. 12
Nov 13 Satisfiability Modulo Theories Text ch. 12
Nov 14 recitation
Nov 18 Guest Lecture: Benjamin Titzer (Virtual Machines?)
Nov 20 Guest Lecture: Ian Dardik (Temporal Logic and Model Checking) supplementary reading
Nov 21 recitation Midterm review
Nov 25 Midterm exam 2
Nov 27 Thanksgiving Break; no class
Nov 28 No recitation
Dec 2 TBD
Dec 4 Review and Project Discussions
Dec 5 recitation
Dec TBD Project Presentations (Time/location TBD)