精确的程序静态分析

程序的静态分析是程序语言和编译领域的一个重要研究方向，已经被研究了很多年。近年来，它也引起形式方法和软件工程领域的重视，被用于程序测试和正确性验证。文中从程序的语法特征、所关心的数据类型和程序性质等方面比较了一些静态分析技术。着重描述基于路径的分析方法，特别是符号执行技术，讨论了程序路径可行性分析问题及其分类、复杂度。针对程序分析精度的一种量化指标，说明了其计算方法。