由于现代程序的日渐复杂大规模，，程序的可靠性也需要理论支持。程序分析成为PL（Programming Language）领域最有活力的方向之一，在程序可靠性、程序安全、编译器优化、程序理解等方面有着很多应用。

静态分析

静态分析在运行一个程序之前，分析它的行为以及判断是否满足一些属性。

Rice’s Theorem

“Any non-trivial property of the behavior of programs in a r.e. language is undecidable.（递归可枚举语言的任何非平凡的性质，都是不可判定的。）

r.e. (recursively enumerable) = recognizable by a Turing-machine

trivial properties 所有程序都有或都没有的性质
non-trivial properties

~= interesting properties
~= the properties related with run-time behaviors of program，如内存泄漏，可优化性

Perfect static analysis不存在

Perfect：Sound AND Complete

Necessity of Soundness

当程序可能出现bug时，我们都应该能够报告错误，即使某些路径上程序可能是正确的

ensure (or get close to) soundness, while making good trade-offs between analysis precision and analysis speed

Abstraction and Over-approximation