CS524: Program Analysis (프로그램 분석)

Notice for Spring 2024

The students who have taken IS593 (Language-based Security) are not eligible to apply.

Logistics

Instructor: Kihong Heo (허기홍, kihong.heo@prosys.kaist.ac.kr)
TAs (mailing list: cs524.ta@prosys.kaist.ac.kr)
- Tae Eun Kim (김태은)
- Geon Park (박건)
Time: Mon/Wed 09:00 - 10:30
Location: N1 102
Office hours:
- Instructor: Mon 10:30 - 11:30
- TAs: Wed 10:30 - 11:30

Course Description

"How to estimate the behavior of a program before it runs?"

This course introduces a technique called program analysis that answers the question. Instead of running programs with potentially infinite inputs, program analysis statically estimates the runtime behaviors of programs within a finite time. The course will cover fundamental theories, designs, and implementations of program analysis including formal semantics of programming languages and the theory of abstract interpretation.

Grading

Homework 50%
Final exam 40%
Participation 10%

This course does not allow for P/NR grading.

Textbook

Lecture slides will be provided
Xavier Rival and Kwangkeun Yi, Introduction to Static Analysis: an Abstract Interpretation Perspective, MIT Press, 2020

Homework

This course includes programming assignments through which students will learn how to design and implement program analyzers. Students will use a few tools which are described here.

All submissions will be managed using Github. For each assignment, a unique invitation URL for GitHub Classroom will be posted in the discussion board. Once you accept the invitation, a private repository for your assignment will be created. You can push as many commits as you want before the deadline. We will grade the final commit of your main branch.

The late homework policy is as follows:

80% credit for one day late
50% credit for two days late
NO credit given after two days late

Academic Integrity Violation

Students who violate academic integrity will get F. See the KAIST CS honor code.

Schedule

#	Topics	Reading	Homework
0	Functional Programming in OCaml		HW0: Hello-world, OCaml Programming
1	Introduction	Chap. 1
2	Operational Semantics	CACM'18, CACM'19, WWDC'21	HW1: Essay
3	Denotational Semantics	Undecidability
4	Concepts in Program Analysis	Chap. 2, Chap. 9	HW2: SmaLLVM Interpreter
5	Abstract Interpretation (1): Concrete Semantics	Chap. 3
6	Abstract Interpretation (2): Abstract Semantics	Chap. 3	HW3: Abstract Interpretation
7	Abstract Interpretation (3): Widening and Narrowing	Chap. 3
8	Design and Implementation of Static Analysis	Chap. 4	HW4: SmaLLVM Analyzer
9	Static Analysis for Advanced Programming Features	Chap. 8.1, Chap. 8.2
10	Advanced Static Analysis Techniques (1): Iteration Techniques	Chap. 5.2	HW5 : ThriLLVM Analyzer
11	Advanced Static Analysis Techniques (2): Sparse Analysis	Chap. 5.3, PLDI'12
12	Advanced Static Analysis Techniques (3): Selective X-sensitivity	PLDI'14
13	Advanced Static Analysis Techniques (4): Modular Analysis	Chap. 5.4, InferBo
14	Specialized frameworks (1): Static Analysis by Equations	Chap. 10.1
15	Specialized frameworks (2): Static Analysis by Monotonic Closure	Chap. 10.2	HW6: SmaLLVM Constraint-based analyzer
16	Specialized frameworks (3): Static Analysis by Proof Construction	Chap. 10.3	HW7: SmaLLVM Type Checker
17	Program Analysis with AI	PLDI'18, PLDI'19, ICSE'19, Trustworthy AI
-	Final Exam