CS 785: Practical program analysis
Fall 2022

Instructor: Martin Kellogg
Office: GITC 4314
Email: martin.kellogg@njit.edu
Office hours: by appointment or immediately after class
Textbook: None required
Class times and location: Tuesday/Thursday, 11:30-12:50, FMH 213
Grading: 50% course project, 35% homework assignments (reading questions and a few programming assignments), 15% participation
How to submit assignments: Canvas

Course Overview: Introduces and contrasts common static program analysis techniques (including abstract interpretation, type systems, heuristic bug-finding, incorrectness logic, verification by reduction to SMT, and more). Students will have the opportunity to gain experience with several program analysis techniques and to gain an intuition for the practical problems that come up when building program analysis tools.

Project Information: This course includes a semester-long research project, which is cumulatively worth 50% of each students grade in the class. Students are permitted to work alone or in teams of up to 3 (I recommend working in a team, because although I will have higher expectations for team projects, students usually report that working together is easier). The main goal of the course project should be to do a (small) research project that is related to one of the themes or topics of the class. I recommend strongly that students draw on their own research interests when choosing a project: I do not mind if you "double-count" the research you were going to do anyway as (part of) your course project, too, as long as it is related to program analysis. While I do expect some novelty in your course projects, the standard is much lower than it would be for e.g., a conference paper. The project itself is structured iteratively: throughout the semester you will submit several versions of a document that will eventually become your final project report. Each project team will also present their project to the class several times during the semester. The most effective way to lower your grade in this course is to ignore the feedback that I give you on these reports and presentations. Even if you disagree with it, please either address it or communicate with me (via email, in-person, etc.) why you disagree.

Course calendar:

Date and Time	Event and Links
Tuesday 9/6/22, 11:30am	Introducton. Please try to come to class in-person today. Join class online; Martin has covid.
Thursday 9/8/22, 11:30am	Heuristic bug finding. Read Lessons from building static analysis tools at Google and answer reading questions on Canvas.
Monday 9/12/22, 11:59pm	HW1 due; submit on Canvas.
Tuesday 9/13/22, 11:30am	Abstract Interpretation. Read "Notes on Program Analysis", sections 2.0 to 2.14, and answer reading questions on Canvas.
Thursday 9/15/22, 11:30am	Abstract Interpretation. Read "Notes on Program Analysis", sections 2.15 to 2.20 and Abstract Interpretation: a semantics-based tool for program analysis, sections 1.0-2.2; skim remainder of section 2. Answer reading questions on Canvas.
Monday 9/19/22, 11:59pm	Project proposals due; submit on Canvas.
Tuesday 9/20/22, 11:30am	Abstract Interpretation. No reading for today.
Thursday 9/22/22, 11:30am	Standard Type Systems. Read Lambda Calculus and "Type Systems", sections 1-4; and answer reading questions on Canvas.
Thursday 9/22/22, 11:59pm	HW2: Part 1 due; submit on Canvas. (HW2 is section 2.21.2 from "Notes on Program Analysis"; part 1 is exercise 29.)
Tuesday 9/27/22, 11:30am	Type Inference. Read Chapter 30 of "Programming Languages: Application and Interpretation" (pages 289-299 in the linked PDF) and Principal type-schemes for functional programs (note that this 1982 paper was re-typeset in 2010 to give a more pleasant reading experience; yes, the paper is famous enough to warrant that; I have linked the re-typeset version, but you may search for the original and read that if you desire); answer reading questions on Canvas.
Thursday 9/29/22, 11:30am	Type Inference 2: Algorithm W. No additional reading.
Thursday 9/29/22, 11:59pm	HW2: Part 2 due; submit on Canvas. (HW2 is section 2.21.2 from "Notes on Program Analysis"; part 2 is exercise 30. Note that this is a programming assignment: start early!)
Monday 10/3/22, 11:59pm	Project proposal resubmission due; submit on Canvas. Your resubmission should accurately reflect your plan for the rest of the semester, taking into account the feedback you got on your original proposal.
Tuesday 10/4/22, 11:30am	Pluggable Type Systems. Read A Theory of Type Qualifiers and Practical Pluggable Types for Java, and answer reading questions on Canvas.
Thursday 10/6/22, 11:30am	Project presentations. Prepare a 15-minute presentation on your revised project proposal, explaining it to your classmates. You will be evaluated both on the content and on the delivery of your presentation. Submit your presentation slides on Canvas at least one hour before lecture.
Tuesday 10/11/22, 11:30am	Typestate Analysis. Skim Typestate: A Programming Language Concept for Enhancing Software Reliability to get the general idea of what typestate is (and its history), and then read Effective Typestate Verification in the Presence of Aliasing and answer reading questions on Canvas.
Thursday 10/13/22, 11:30am	Accumulation Analysis. Read Accumulation Analysis, then skim Verifying Object Construction to see an example of an accumulation analysis in practice,, and then answer reading questions on Canvas.
Tuesday 10/18/22, 11:30am	Floyd-Hoare Logic. Read Jonathan Aldrich's Notes on Hoare Logic and then Classical Program Logics: Hoare Logic, Weakest Liberal Preconditions, and answer reading questions on Canvas.
Thursday 10/20/22, 11:30am	Verification by reduction to SMT: what is SAT-solving?. Skim Chapter 1 of "Calculus of Computation", sections 1 to 1.6 (pages 2-21 in the PDF) to make sure you understand the basics of propositional logic. Then read the remainder of chapter 1 (section 1.7, pages 21-31) in detail. Then answer reading questions on Canvas.
Tuesday 10/25/22, 11:30am	Guest Lecture: Equality Saturation. Max Willsey will give a guest lecture on his work on e-graphs and equality saturation. No reading for today.
Thursday 10/27/22, 11:30am	Verification by reduction to SMT: using an SMT solver. Read Programming Z3 (pages 165-214 in the PDF; it's not as long as it seems). Then answer reading questions on Canvas.
Tuesday 11/01/22, 11:30am	Verification by reduction to SMT: SMT-based tools. Read Extended Static Checking For Java. Then answer reading questions on Canvas.
Tuesday 11/01/22, 11:59pm	Project checkpoint 1 report due; submit on Canvas.
Thursday 11/03/22, 11:30am	Reduction to graph reachability: IFDS Skim Precise Interprocedural Dataflow Analysis via Graph Reachability, focusing on understanding the idea of the core algorithm rather than the specific details provided in the paper. Then, read Inter-procedural data-flow analysis with IFDS/IDE and Soot; you should understand IFDS well-enough to make sense of section 2. Then answer reading questions on Canvas.
Tuesday 11/8/22, 11:30am	Applications of IFDS. Read FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps and answer reading questions on Canvas.
Thursday 11/10/22, 11:30am	Unsoundness. Read In Defense of Soundiness: A Manifesto and An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer, and answer reading questions on Canvas.
Tuesday 11/15/22, 11:30am	Martin out of town: Iulian will guest lecture. Read Contextual Effects for Version-Consistent Dynamic Software Updating and Safe Concurrent Programming and answer reading questions on Canvas.
Thursday 11/17/22, 11:30am	Martin out of town: Iulian will guest lecture. Read Automatically Verifying and Reproducing Event-Based Races in Android Apps and Static Detection of Event-based Races in Android Apps and then answer reading questions on Canvas.
Tuesday 11/22/22, 11:30am	Project status presentations. Prepare a 15+5 presentation (i.e., 15 minutes of you talking, and 5 minutes for questions) about the current state of your course project. Be sure to update the class on any changes you've made to the project itself as well as on your progress so far. Submit your slides on Canvas at least one hour before lecture.
Thursday 11/24/22, 11:30am	No class: Thanksgiving.
Tuesday 11/29/22, 11:30am	Unsoundness in practice. Read NullAway: Practical Type-Based Null Safety for Java and Rapid: Checking API Usage for the Cloud in the Cloud and answer reading questions on Canvas.
Tuesday 11/29/22, 11:59pm	Project checkpoint 2 report due; submit on Canvas.
Thursday 12/1/22, 11:30am	Incorrectness Logic. Read Incorrectness Logic and answer reading questions on Canvas.
Tuesday 12/6/22, 11:30am	Topic: Array Bounds Analysis. Read Clousot: Static Contract Checking with Abstract Interpretation (focus on their handling of arrays, which is what we'll discuss in class) and Lightweight Verification of Array Indexing, and answer reading questions on Canvas.
Thursday 12/8/22, 11:30am	Topic: Resource Leak Analysis. Read Grapple: A Graph System for Static Finite-State Property Checking of Large-Scale Systems Code (focusing on how they handle resource leaks) and Lightweight and Modular Resource Leak Verification, and answer reading questions on Canvas.
Tuesday 12/13/22, 11:30am	Topic: Analysis of Uses of Cryptography. Read CRYSL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs and Continuous Compliance (focus on their handling of correct use of cryptography, especially the comparison experiment in section 7), and answer reading questions on Canvas.
Tuesday 12/13/22, 11:59pm	Project final report (draft) due; submit on Canvas.
Monday 12/19/22, 2:30pm	Final exam (final presentations) and course wrapup. Prepare a 15+5 presentation on your final course project results. Submit your slides on Canvas at least one hour before the exam. Location: CKB 223
Tuesday 12/20/22, 11:59pm	Project final report resubmission due; submit on Canvas.