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

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 RecitationCodeQL Notes
Jan 21 Dataflow Analysis and Abstract Interpretation PPA ch. 2
Jan 23 Dataflow Analysis and Abstract Interpretation, continued hw1 Repository PPA ch. 6
Jan 24 RecitationSemantics
Jan 28 Dataflow Analysis examples
Jan 30 Dataflow Analysis examples (continued) hw2
Jan 31 recitationSpecifying/Implementing Dataflow Analysis
Feb 4 Dataflow Analysis termination and complexity PPA ch. 4
Feb 6 Widening and collecting hw3
Feb 7 RecitationProving correctness
Feb 11 Interprocedural analysis
Feb 13 Declarative Program Analysis hw4
Feb 14 RecitationDatalog
Feb 18 Control Flow Analysis
Feb 20 OO Call Graph Construction hw5
Feb 21 RecitationMidterm review
Feb 25 Midterm 1
Feb 27 Hoare-style verification
Feb 28 RecitationHoare-style verification
Mar 3 Hoare-style verification (continued)
Mar 5 Likely: Guest Lecture
Mar 6 no recitationMid-Semester Break
Mar 10 No class, Spring Break
Mar 12 No class, Spring Break
Mar 13 No recitation Spring Break
Mar 17 Separation Logic
Mar 19 Symbolic execution hw6
Mar 20 recitation Symbolic execution
Mar 24 Concolic execution and test generation
Mar 26 Satisfiability Modulo Theories hw7
Mar 27 RecitationZ3/SMT
Mar 31 Program synthesis
Apr 2 Program synthesis, continued project proposal
Apr 3 RecitationSynthesis
Apr 7 Program repair
Apr 9 Program repair, continued hw8
Apr 10 RecitationTBA
Apr 14 Midterm 2
Apr 16 No lecture: Spring Carnival
Apr 17 no recitationSpring Carnival
Apr 21 Dynamic Analysis for Data Race Detection
Apr 23 Likely: Guest Lecture Project checkpoint
Apr 24 RecitationTBA
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