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: TBD
Email: rohanpadhye@cmu.edu
Headshot of Professor Rohan Padhye
TA: Bella Laybourn
Zoom
Office hours: Wed. 1:45-2:45pm ET
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).

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 Remote PPA ch. 1
Jan 20 Program Semantics Text ch. 3 Remote
Jan 21 recitation CodeQL Remote
Jan 25 Dataflow Analysis and Abstract Interpretation Text ch. 4 Remote PPA ch. 2
Jan 27 Dataflow Analysis and Abstract Interpretation (contd.) Text ch. 4 hw1 Remote PPA ch. 6
Jan 28 recitation Semantics Remote
Feb 1 Dataflow Analysis examples Text ch. 5
Feb 3 Dataflow Analysis examples (contd.) Text ch. 5 hw2
Feb 4 recitation Specifying/Implementing Dataflow Analysis
Feb 8 Dataflow Analysis - Termination and Correctness Text ch. 6
Feb 10 Widening Operators and Collecting Semantics Text ch. 7 hw3
Feb 11 recitation Data-Flow Analysis Correctness
Feb 15 Interprocedural analysis Text ch. 8
Feb 17 Context-Sensitive Analysis Text ch. 8 hw4
Feb 18 recitation
Feb 22 Control-Flow Analysis for Functional Languages Text ch. 9
Feb 24 Pointer Analysis Text ch. 10 hw5 checkpoint
Feb 25 recitation Midterm review
Mar 1 Mid-term exam midterm
Mar 3 hw5
Mar 4 no recitation
Mar 7—11 Spring Break; no classes
Mar 15
Mar 17
Mar 18
Mar 22
Mar 24
Mar 25
Mar 29 hw6
Mar 31
Apr 1
Apr 5 hw7
Apr 7 Spring carnival; no class
Apr 8 no recitation
Apr 12
Apr 14 hw8 (incl. project proposal)
Apr 16
Apr 19
Apr 21
Apr 22
Apr 26
Apr 28
Apr 29
May 2—9 (TBD) Project Presentations
May 2—9 (TBD) project final report due