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

(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

Professor Rohan Padhye
TCS 325
Office hours: Tue. 4:00—5:00pm ET
Email: rohanpadhye@cmu.edu
Headshot of Professor Rohan Padhye
TA: Bella Laybourn
Office hours: Wed. 1:45—2:45pm ET via Zoom
Email: ilaybour@andrew.cmu.edu
Headshot of teaching assistant Bella Laybourn

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 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 +
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)
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
Apr 29 recitation Project Discussions Remote
May 9 (1-4pm) Project Presentations In-Person
(GHC 4307)
May 9 (midnight) project final report
same pdf