COL 862: SPECIAL TOPICS IN SOFTWARE SYSTEMS

Applied Program Analysis


Timing: TBD

Venue: TBD

Instructor: Soham Chakraborty

Prerequisite:

UG graph theory and algorithms, discrete structures.
Any additional knowledge on programming languages, compilers, formal methods, and related topics would be useful but not assumed.

Motivation

Program analysis discovers various properties about programs which is used in program optimization and program correctness, and has been a key area in computer science. Like many interesting problems, program analysis is undecidable in general. "However, just because a problem is hard does not mean it never appears in practice. Also, just because the general problem is undecidable does not imply that specific instances of the problem will also be hard."[1]

To address this challenges of program analysis techniques and tools have been developed by academia, industry, and open-source communities over the years and state-of-the-art program analyzers scales to larger programs and reveals more interesting properties. These analyzers are regularly used in industry and have demonstrated measurable success in improving programmers' productivity.

In this course we will study the foundational theories and engineering challenges involved in some of these program analyzers. We will also discuss some challenges and lessons in developing industry scale program analyzers [2, 3, 4, 5, 6].

Course structure:

The course content (and the order) is flexible and will progress based on common interest. We will explore various types of program analysis techniques from static and dynamic analysis as well as program verification techniques along with state-of-the-art analyzers such as CPROVER, Infer, Clang sanitizers and so on.

Course objective:

On successful completion of the course, a student will be familiar with program analysis techniques with hands-on experience on latest program analysis tools.

Grading:

Grading will be relative. Tentative scheme: assignments including paper reading (30%), projects (50%), and exams (20%).

Course materials, Lectures, announcements

Follow the course page in moodle.

Schedule

Date Topic
28.09.2020 Introduction
01.10.2020 program structure (syntax tree and Control Flow Graph)
05.10.2020 Control Flow Graph, Loops
08.10.2020 Introduction to LLVM

Some readings/References:

[1] Software Model Checking. Ranjit Jhala and Rupak Majumdar. CSUR 2009.

[2] From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. M Harman and P O'Hearn. Invited paper at SCAM'18.

[3] Experience developing and deploying concurrency analysis at Facebook. Peter O'Hearn. Invited tutorial at SAS'18.

[4] Continuous Reasoning: Scaling the impact of formal methods. Peter O'Hearn. LICS'18.

[5] Lessons from Building Static Analysis Tools at Google. By Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, Ciera Jaspan. CACM, 2018.

[6] Microsoft rise4fun. https://rise4fun.com/