Type of Credit: Elective
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 should have familiarity with Python programming and a basic understanding of discrete mathematics and data structures. The course includes weekly lab sessions, and 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:
|
週次 Week |
課程內容與指定閱讀 Content and Reading Assignment |
學習投入時間 Student workload expectation |
|
|
課堂講授 In-class Hours |
課程前後 Outside-of-class Hours |
||
|
1 |
(9/5) Program Representations: AST, IR, CFG, stack machines
|
3 |
6 |
|
2 |
(9/12 - 9/19) Dataflow Analysis: theoretical framework, sample analyses, soundness and correctness, termination and complexity
|
3 |
6 |
|
3 |
3 |
6 |
|
|
4 |
(9/26 - 10/3) Constraint Programming: Satisfiability Modulo Theories, SAT and SMT encoding, Z3
(10/10) Holiday
|
3 |
6 |
|
5 |
3 |
6 |
|
|
6 |
3 |
6 |
|
|
7 |
(10/17) Midterm Exam (Exam date may change according to course progress)
|
3 |
6 |
|
8 |
3 |
6 |
|
|
9 |
|
3 |
6 |
|
10 |
(11/7 - 11/21) Deductive Verification: axiomatic semantics, weakest preconditions, Floyd-Hoare proofs |
3 |
6 |
|
11 |
3 |
6 |
|
|
12 |
3 |
6 |
|
|
13 |
(11/28) Final Exam (Exam date may change according to course progress)
(12/5 - 12/12) Topics on AI for SE: Enhancing program analysis and testing using neural networks and large language models
|
3 |
6 |
|
14 |
3 |
6 |
|
|
15 |
3 |
6 |
|
|
16 |
(12/19) Final Project Demo |
3 |
6 |
Assessments
Participation 10%
Homework 10%
Midterm exam 30%
Final exam 30%
Final project 20%
Class participation plays a key role, as lectures are the primary means of conveying course material, which is then reinforced through in-class activities. Participation points are earned by completing these exercises in person.
The assignments are designed to help students develop theoretical understanding and practical skills in program analysis.
The exams mainly consist of variations of in-class and homework exercises that evaluate your understanding of the material.
The final project involves implementing a simple program analyzer. The expected deliverables include coding, documentation, and a presentation.