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?
- Explore the meaning of programs. One of the most basic questions that programmers ask is "What does this program do?" Program analysis is all about understanding programs--automatically!
- Learn deep theory. The theory of abstract interpretation stands with type theory as the most important and beautiful foundations of programming languages. Abstract interpretation is the fundamental theory of abstraction: how to precisely relate the concrete execution of a program to an abstraction of that execution. Naturally, this has many applications, which brings us to the third reason to take this course:
- Build awesome tools. Using program analysis, you can build tools that find bugs, prove important security and correctness properties, automatically generate useful tests, and much more--and you'll have a chance to do all of this in course assignments and a project that you can design yourself (if you want).
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
WEH 5117
Office hours: Tu 3:00 - 4:00, or by appointment
Email: clegoues@cs.cmu.edu
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 | notes, slides | ||
| Apr 2 | Program synthesis, continued | hw7 hw7.pdf | ||
| Apr 3 | recitation Synthesis | repository | ||
| Apr 7 | Program repair | slides | ||
| Apr 9 | Program repair, continued | notes, slides | hw8 hw8.pdf (incl. project) proposal) | |
| Apr 10 | recitationMidterm review | |||
| Apr 14 | Office Hours | |||
| Apr 16 | Separation Logic | Primer on Separation Logic | ||
| Apr 17 | no recitation | |||
| Apr 21 | Model Checking (1/2) | slides | ||
| Apr 23 | Model Checking (2/2) | slides | Project checkpoint | |
| Apr 24 | recitation TBA | |||
| Apr 28 | Model Checking | |||
| Apr 30 | Counterexample-Guided Abstraction Refinement in Blast | |||
| May 1 | no recitation | |||
| May 8, 1pm-4pm | Project presentations | Project presentations | ||
| May 11 | project final report due |