Program Analysis
- Level
- Undergraduate
- Status
- Under development
Note: this course is still being designed and calibrated; the page content is for reference and does not represent the final teaching version.
Syllabus
Course Overview
Program Analysis studies how to automatically reason about program behavior. The course covers control flow, data flow, abstract interpretation, pointer analysis, symbolic execution, constraint solving, and static security checks, requiring students to implement a tool that analyzes real small programs.
This is the algorithmic and tooling bridge among software security, system security, and protocol verification.
Prerequisites
- Compilers or equivalent AST/IR background.
- Discrete mathematics and basic algorithms.
- Familiarity with a language suitable for implementing analyzers.
Learning Outcomes
- Construct CFGs, call graphs, and data-flow facts.
- Implement classic data-flow analyses and abstract interpretation.
- Understand tradeoffs among precision, scalability, and soundness.
- Use constraint solving or symbolic execution to find path problems.
- Design a static security checker and evaluate false positives and false negatives.
Course Format
- Two meetings per week: one for core concepts and one for labs, paper discussion, or project review.
- The course proceeds over 16 weeks, each with a checkable assignment, lab, or project milestone.
- Reproducibility is required: code, configuration, data, lab logs, and reports must be reviewable by staff or peers.
Weekly Plan
Program representations and analysis problems
Construct ASTs, IR, and CFGs.
Program representations and analysis problems: lab and review
Construct ASTs, IR, and CFGs. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Data-flow analysis framework
Implement liveness or reaching-definitions analysis.
Data-flow analysis framework: lab and review
Implement liveness or reaching-definitions analysis. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Abstract interpretation and lattices
Implement interval or symbolic-set analysis.
Abstract interpretation and lattices: lab and review
Implement interval or symbolic-set analysis. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Pointers, aliasing, and heap abstraction
Compare context-sensitive and insensitive analyses.
Pointers, aliasing, and heap abstraction: lab and review
Compare context-sensitive and insensitive analyses. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Interprocedural analysis and call graphs
Extend the analyzer to handle function calls.
Interprocedural analysis and call graphs: lab and review
Extend the analyzer to handle function calls. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Symbolic execution and constraint solving
Generate inputs that trigger selected paths.
Symbolic execution and constraint solving: lab and review
Generate inputs that trigger selected paths. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Security checks and alert ranking
Implement a taint or API-misuse checker.
Security checks and alert ranking: lab and review
Implement a taint or API-misuse checker. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Analyzer evaluation
Submit benchmarks, false-positive analysis, and improvement plan.
Analyzer evaluation: lab and review
Submit benchmarks, false-positive analysis, and improvement plan. Complete the paired lab, record issues, and explain design tradeoffs in class review.
Assessment
Concept questions, reading responses, design tasks, and small programming or lab exercises.
Analyzer implementation, benchmarks, alert evaluation, and report.
Participation in discussions, demos, code or paper reviews, and peer feedback.
Submit reproducible artifacts, a technical report, and a demo explaining methods, results, limitations, and future work.
Course Project
Students implement a static analyzer or symbolic-execution tool for real code snippets, with algorithm notes, benchmarks, false-positive and false-negative analysis, and usage docs.
Policies
- AI tools are allowed, but generated code, lab notes, and design suggestions must be reviewed by the student and disclosed in the report.
- Students may not submit code, proofs, configuration, or experimental results they cannot explain; each member must defend their own design, tests, and tradeoffs.
- Late work affects iteration grades, but the course values reproducible, auditable, and maintainable results over last-minute accumulation.
Reference Courses
International
- CMU17-355/17-665: Program Analysis
- CornellCS 6120: Advanced Compilers
- ETH ZurichProgram Analysis for System Security and Reliability
- Georgia TechCS 6340: Software Analysis and Test
- MIT6.820 Fundamentals of Program Analysis
- PrincetonCOS 516: Automated Reasoning about Software
- StanfordCS 243: Program Analysis and Optimizations
- UC BerkeleyCS 294-260: Program Analysis and Optimization
- University of WashingtonCSE 503: Software Engineering
China 985 Universities
- 上海交通大学CS 2612: Programming Languages and Compilers
- 中国科学技术大学程序语言设计与程序分析
- 北京大学软件分析技术
- 南京大学软件分析（Software Analysis）
- 复旦大学智能化软件工程与系统
- 清华大学程序分析