精确的程序静态分析

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

Sharp Static Analysis of Programs

Static program analysis has been studied for many years.It is an important topic in the research of programming languages and compilers.Recently,it has also attracted researchers from other areas such as formal methods and software engineering,and some ideas have been used for program verification and testing.This paper compares various static analysis techniques,according to the syntactic features,data types and correctness properties targeted by the techniques.The paper focuses on a class of analysis techniques that are based on program paths,especially symbolic execution;discusses the path feasibility problem,its difficulty and its subproblems.A method for computing a data coverage measure of paths is also described.