Type of Credit: Partially Required
Credit(s)
Number of Students
This course introduces foundational skills in program analysis and testing, which are essential for building software systems with greater reliability and security. The course examines primarily two complementary approaches: static analysis, where we analyze source code without execution to uncover potential security vulnerabilities, and dynamic analysis, where we study program behavior during runtime to detect actual security breaches. Students will learn to bridge theory and practice by implementing these analyses using modern tools and frameworks.
Prospective students are expected to have a strong background in Python programming and a basic knowledge of discrete mathematics and data structures. The course includes weekly lab sessions; students may need a laptop to participate in some of these sessions.
能力項目說明
We assess the achievement of learning objectives through classroom discussions and exercises, assignments, a midterm exam, and a final project. These objectives include:
Technical Skills in Program Analysis: Students will learn to implement various program analysis techniques including dataflow analysis, Hoare logic, symbolic execution, and dynamic analysis. They will also explore how abstract interpretation principles can automate program analysis frameworks.
Formal Methods and Evaluation: Students will gain the ability to use abstract interpretation to formally prove the soundness and termination of an analysis. They will also learn to evaluate the scalability of program analyses and compare the precision of different techniques.
General Computer Science Skills: The course also focuses on developing transferable skills, such as:
| 教學週次Course Week | 彈性補充教學週次Flexible Supplemental Instruction Week | 彈性補充教學類別Flexible Supplemental Instruction Type |
|---|---|---|
|
週次 Week |
課程內容與指定閱讀 Content and Reading Assignment |
學習投入時間 Student workload expectation |
|
|
課堂講授 In-class Hours |
課程前後 Outside-of-class Hours |
||
|
1 |
(2/21) Program Representations: AST, IR, CFG, stack machines |
3 |
6 |
|
2 |
(2/28) Holiday (3/7) Program Semantics: operational semantics |
3 |
6 |
|
3 |
3 |
6 |
|
|
4 |
(3/14 - 3/28) Dataflow Analysis: theoretical framework, sample analyses, soundness and correctness, termination and complexity |
3 |
6 |
|
5 |
3 |
6 |
|
|
6 |
3 |
6 |
|
|
7 |
(4/4) Holiday (4/11-4/25) Constraint Programming: Satisfiability Modulo Theories, SAT and SMT encoding, problem solving with Z3 |
3 |
6 |
|
8 |
3 |
6 |
|
|
9 |
(5/2) Midterm Exam |
3 |
6 |
|
10 |
(5/9 - 5/23) Floyd-Hoare Proof System: axiomatic semantics, strongest postconditions and weakest preconditions, deductive verification |
3 |
6 |
|
11 |
3 |
6 |
|
|
12 |
3 |
6 |
|
|
13 |
(5/30) Holiday (6/6 - 6/13) Coverage Analysis: white-box and grey-box testing, fuzzing, symbolic and concolic execution |
3 |
6 |
|
14 |
3 |
6 |
|
|
15 |
3 |
6 |
|
|
16 |
(6/20) Final Project Demo |
3 |
6 |
Assessments
Participation 10%
Exercises & assignments 40%
Midterm exam 20%
Final project 30%
Total: 100%
Class participation and readings play a key role, as lectures and readings are the primary means of conveying course material, which is then reinforced through in-class activities. Most class sessions will include an exercise designed to help students apply the concepts covered. Participation is earned by completing these exercises, regardless of the correctness of the responses.
Assignments are designed to help students develop theoretical understanding and practical skills in program analysis. They are divided into two categories:
Theoretical Assignments: These assignments involve formal definitions and proofs to deepen your understanding of the analysis theory. They will be graded based on the accuracy and presentation of your definitions and proofs.
Programming Assignments: These focus on building program analyses systematically through hands-on coding exercises. Your work will be evaluated based on the correctness and clarity of your implementation.
The final project involves implementing a simple program analyzer. The expected deliverables include coding, documentation, a presentation, and a demonstration.
| 書名 Book Title | 作者 Author | 出版年 Publish Year | 出版者 Publisher | ISBN | 館藏來源* | 備註 Note |
|---|