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

Note: This course will next be offered in Fall'24 and every Fall thereafter.

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 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

Professor Claire Le Goues
TCS 363
Office hours: Friday 1 - 2 pm
Email: clegoues@cs.cmu.edu
Headshot of Professor Claire Le Goues
Professor Fraser Brown
CIC 2218
Office hours: Tuesday 1:30-2:30 pm
Email: fraserb@andrew.cmu.edu
Headshot of Professor Fraser Brown
TA: Daniel Ramos
TCS 347
Office hours: Thursday 9:30-10:30 am (TCS 347)
Email: danielrr@cmu.edu
Headshot of teaching assistant Daniel Ramos

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).


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