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.

Why take this course?

Logistics and People

Class Tu/Th 10:30 - 11:50 a.m. in GHC 4211
Recitation F 1:30 - 2:20 p.m. in WEH 5415
Spring 2020
12 units

Professor Claire Le Goues
WEH 5117
Office hours: Tu 3:00 - 4:00, or by appointment
Email: clegoues@cs.cmu.edu
Headshot of Professor Claire Le Goues

TA: Jeremy Lacomis
WEH 5119
Office hours: W 12:30 - 1:30
Email: jlacomis@cmu.edu
Headshot of teaching assistant Jeremy Lacomis

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 2020, 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 Optional Reading
Jan 14 Introduction, Program Representation, and Syntactic Analysis notes, slides, in-class exercises PPA ch. 1
Jan 16 Program Semantics notes, in-class exercises
Jan 17 recitation CodeQL notes
Jan 21 Dataflow Analysis and Abstract Interpretation notes PPA ch. 2
Jan 23 Dataflow Analysis and Abstract Interpretation, continued in-class exercises hw1 Repository PPA ch. 6
Jan 24 recitation Semantics in-class exercises, notes
Jan 28 Dataflow Analysis examples notes, in-class exercises
Jan 30 Dataflow Analysis examples (continued) hw2 hw2.pdf mathpartir
Jan 31 recitation Specifying/Implementing Dataflow Analysis
Feb 4 Dataflow Analysis termination and correctness notes, in-class exercises PPA ch. 4
Feb 6 Widening and collecting notes
Feb 7 recitation Proving correctness notes, in-class exercises
Feb 11 Interprocedural analysis notes, in-class exercises hw3 hw3.pdf
Feb 13 Control Flow Analysis notes, in-class exercises PPA ch. 3
Feb 14 recitation Introduction to Soot repository
Feb 18 CFA (continued); Pointer analysis notes, in-class exercises hw4 hw4.pdf
Feb 20 Pointer analysis and OO Call Graphs
Feb 21 recitation Midterm review
Feb 25 Midterm 1 study guide
Feb 27 Hoare-style verification notes, in-class exercises
Feb 28 recitation Hoare-style verification in-class exercises
Mar 3 Hoare-style verification (continued)
Mar 5 Optional Bonus Office Hours hw5 hw5.pdf
Mar 6 no recitation Mid-Semester Break
Mar 10 No class, Spring Break
Mar 12 No class, Spring Break
Mar 13 no recitation Spring Break
Mar 17 No Class
Mar 19 Symbolic execution notes
Mar 20 recitation Symbolic execution
Mar 24 Concolic execution and test generation notes,slides hw6 hw6
Mar 26 Satisfiability Modulo Theories notes
Mar 27 recitation Z3/SMT repository
Mar 31 Program synthesis
Apr 2 Program synthesis, continued hw7 hw7.pdf
Apr 3 recitation Synthesis
Apr 7 Program repair
Apr 9 Program repair, continued hw8 (w/project proposal)
Apr 10 recitationMidterm review
Apr 14 Likely: Separation Logic
Apr 16 Midterm 2
Apr 17 TBA
Apr 21 Likely: Declarative program analysis
Apr 23 Likely: Dynamic Analysis Project checkpoint
Apr 24 recitation TBA
Apr 28 Model Checking
Apr 30 Counterexample-Guided Abstraction Refinement in Blast
May 1 no recitation
Finals week Project presentations Project presentations
May TBA project final report due