静态程序分析技术是一门通过静态分析程序的源代码来推到程序在执行时所具有的行为属性的技术。理论上讲，静态程序分析只能推导出程序中某些性质的近似解，而不能得到精确解。在静态程序分析器设计中的一个重要问题是如何在分析结果的精确性和分析的代价中取得平衡。静态程序分析技术最初的应用是编译器优化，即将程序的一种形式，在保持其某些性质不变的前提下，转化为另一种形式。虽然编译器的优化一直是程序静态分析的主要应用，但随着时间的推移，静态分析技术也越来越多地应用于软件开发工具中，如程序理解工具、重构工具、以及测试和验证工具等。 本课程将重点介绍程序静态分析的基本原理以及目前在相关领域中的最新研究成果。本课程将在课堂上着重讨论程序静态分析的经典论文及最新的研究论文，并将结合所讲授的知识要求学生完成一个大作业项目以加深对课堂所学知识的理解和活用。

A static program analysis aims to prove properties about the runtime behaviour of a program without actually running it. Since interesting properties are undecidable in general, static analyses provide only an approximation. A pervasive issue in the design of static analyses is the trade-off between precision (i.e. the number of programs satisfying a property for which the property can be proven) and the cost of the analysis. Static analysis was originally motivated by the needs of optimizing compilers, which transform programs in ways that preserve their behaviour. Compilation continues to be an important application area for static analysis. Increasingly, static analysis is also applied in software development tools, such as program understanding tools, refactoring tools, testing and verification tools. This course covers both fundamental concepts and recent research in program analysis through in-class discussions of key publications in the area. While the in-class portion of the course focuses on program analyses themselves, the project portion is more flexible, and interested students are encouraged to explore applications of program analysis in their projects.