Skip to content

phlummox-dev/cs524-program-analysis

 
 

Repository files navigation

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

Logistics

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 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%

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 issue 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'19 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): Wideining 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

About

clone of program analysis course content from @prosyslab-classroom

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Python 100.0%