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)
- 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
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 ![](https://github.com/prosyslab-classroom/cs524-program-analysis/raw/main/icons/eng.png) |
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 |
Hall of Fame
Have fun with student artifacts from previous semesters here (distinguished essays, drawings, etc).
References
- PL Wiki
- Static Analysis in the Real World