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?
- 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: Tue/Thu 11:00 a.m. — 12:20 p.m. in GHC 4101
Recitation: Fri 10:00 a.m. — 10:50 a.m. in WEH 5320
Fall 2024
12 units
Office hours:
Tues 10:00-10:45 a.m., TCS 316
Wed 2:45-3:30pm, TCS 316
Email: idardik@andrew.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 August 2024, 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 | HW Due | Optional Reading | |
|---|---|---|---|---|---|
| Aug 27 | Introduction, Program Representation, and Syntactic Analysis | Text ch. 1 & 2 | PPA ch. 1 | ||
| Aug 29 | Program Semantics | Text ch. 3 | |||
| Aug 30 | recitation CodeQL | ||||
| Sep 3 | Program Semantics (cont.) | ||||
| Sep 5 | Program Semantics (cont.) | hw1 | PPA ch. 2 & 6 | ||
| Sep 6 | recitation Semantics | ex1, ex2 | |||
| Sep 10 | Dataflow Analysis & Abstract Interpretation Framework | Text ch. 4 | PPA ch. 2.1 | ||
| Sep 12 | Dataflow Analysis examples | Text ch. 5 | hw2 pdf mathpartir | PPA ch. 2 | |
| Sep 13 | recitation Specifying/Implementing Dataflow Analysis | ||||
| Sep 17 | Dataflow Analysis examples (cont.) | PPA ch. 2.2—2.3 | |||
| Sep 19 | Termination and Correctness | Text ch. 6 | hw3 pdf | PPA ch. 2.3—2.4 | |
| Sep 20 | recitation Data-Flow Analysis Correctness | notes, sol2, sol2det, sol3 | |||
| Sep 24 | Termination and Correctness | PPA ch. 2.5 | |||
| Sep 26 | Precision and Widening | Text ch. 7 | hw4 pdf (due 9/30) | PPA ch. 2.5 | |
| Sep 27 | recitation | repo | |||
| Oct 1 | Interprocedural analysis | Text ch. 8 | |||
| Oct 3 | Context-Sensitive Analysis | Text ch. 8 & ch. 10.2 | |||
| Oct 7 (not Oct 4!) | recitation Midterm review. Class will be in TCS460 @ 1pm | Midterm Study Guide | |||
| Oct 8 | Pointer Analysis + Call Graphs for Object-Oriented Languages | Text ch. 10 | hw5 checkpoint pdf | PPA ch. 3 | |
| Oct 10 | Midterm exam 1 | midterm | |||
| Oct 11 | no recitation | ||||
| Oct 14—18 | Fall Break; no classes | ||||
| Oct 22 | Intro to Hoare Logic | Text ch. 11 | |||
| Oct 24 | Verification using Hoare Logic | Text ch. 11 | hw5 | ||
| Oct 25 | recitation Hoare Logic Proofs using Axiomatic Semantics | notes, solutions | |||
| Oct 29 | Symbolic Execution | Text ch. 13 | |||
| Oct 31 | Concolic Testing | Text ch. 14 | hw6 pdf | ||
| Nov 1 | recitation Midterm 1 review | ||||
| Nov 5 | Democracy Day; no class | ||||
| Nov 7 | Satisfiability Modulo Theories | Text ch. 12 | hw7 pdf (due 11/11) | ||
| Nov 8 | recitation Intro to Z3 | repo | |||
| Nov 12 | Satisfiability Modulo Theories (cont.) | ||||
| Nov 14 | Program Synthesis | Text ch. 15 | project proposal project instructions |
||
| Nov 15 | recitation Simple synthesis using Z3 | repo ex2-sol (w/bug) ex2-synth | |||
| Nov 19 | Program Repair (guest lecture by Claire Le Goues) | ||||
| Nov 21 | Temporal Logic and Model Checking (guest lecture by Ian) | hw8 pdf | |||
| Nov 22 | recitation Midterm review | ||||
| Nov 26 | Midterm exam 2 | midterm | |||
| Nov 28 | Thanksgiving Break; no class | ||||
| Nov 29 | No recitation | ||||
| Dec 3 | Dynamic Analysis (Fuzz Testing, Invariant Generation) | Text ch. 16 | |||
| Dec 5 | Review and Project Discussions | project checkpoint | |||
| Dec 6 | recitation Dynamic analysis on stack machine bytecode | ||||
| Dec 13 | Project Presentations (5:30-8:30pm) | ||||
| Dec 13 | project final report |
