¡¡	Chinese Journal of Computers   Full Text
Title	Sharp Static Analysis of Programs
Authors	ZHANG Jian
Address	(State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190)
Year	2008
Issue	No.9(1549¡ª1553)
Abstract &   Background	Abstract 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. Keywords static analysis; program paths; symbolic execution; data coverage Background Program correctness has been a central issue in computer science for many decades, and it has also become a serious concern for software engineers. To ensure the correctness of programs, many formal verification methods have been proposed, but they are often difficult to use in practice. In industry, engineers typically rely on testing to find bugs. In contrast to the above two methods, static analysis techniques try to find specific types of bugs in a program, automatically and efficiently, without running the program. Tools based on such techniques have been quite helpful to programmers. However, to deal with big programs, most of the techniques try to abstract away some aspects of the program which are not so relevant. This may bring various kinds of false warnings. This paper compares some of these techniques, and argues that we should pay more attention to more advanced, more accurate analysis methods. As an example of such methods, symbolic execution is described in detail. We believe that it is a promising way of analyzing programs accurately. Some research issues are also discussed. This work is partially supported by the National Natural Science Foundation of China (NSFC) under grant Noª±60673044 and Noª±60633010, and by the National High-Tech Program (863) under grant Noª±2006AA01Z402.