An Integration Of Several Data Flow Analysis Techniques For Program Verification

In interactive program verification processes, people want to derive some program prop-erties automatically to improve the verification efficiency. Data flow analysis is a set of static program analysis techniques. It can be used in program verification processes. However, most of the existing dataflow analysis techniques work separately. This will make program prop-erties cannot be sufficiently extracted using several dataflow analysis tools separately. Most existing dataflow analysis techniques are fully automated processes. Users cannot participate in the analysis processes. Sometimes, the lackness of the key information may prevent the current data flow analysis techniques from extracting more useful properties. Accordingly, in order to enhance the ability of data flow analysis techniques, we should make them to be able to interact with each other, and allow the users to guide data flow analysis processes by giving key properties.In this paper, in order to promote a better integration of data flow analysis techniques, we put forward a platform together with a set of methods. A prototype tool has been developed. It integrates three typical data flow analysis techniques:null pointer dereference analysis, integer variable value interval analysis and the single-linked list reachability analysis, and offer the ability to interact with users. And at last, two cases are provided to demonstrate the value of this work. This paper has mainly solved the following problems:· How to specify the various program properties. Existing data flow analysis tech-niques concern about different kinds of program properties. We defined a unified form to represent these properties. In addition, for the recursively defined data structures, we use recursive functions to describe the characters. Otherwise, the dependencies be-tween program properties are also stored in order to facilitate the understanding by the users.· How to re-use the results of dataflow analysis techniques. In order to better describe the program characters, control flow graphes are used as the central data structure in our platform. All of the program properties are stored in assert-points, which are points between program statements. In every assert-point, program properties can be inserted,...