Treffer: Space-Aware Data Flow Analysis

This paper may not be, either entirely or in part, published and distributed without the explicit permission of the authors. It supersedes [2] analysis. In this paper we propose a method to reduce space usage during some kind of DFA analysis. The method proceeds as follows: first, we define a formal proof system for sentences like "all execution paths that start at node n, with initial execution state f , and reach node m, have been tried"; the rules in the proof deduce sentences about sets of paths, based on the validity of sentences on sub-paths. We show that every proof in our system contains an approximation of the information collected at nodes when all paths are executed. Then, we give an algorithm to find proofs in our system. The algorithm constructs the proof in a goal directed (or backward) fashion. The algorithm has the potential to save space since it can release some program state information each time it has constructed a proof for a sub-goal. This space saving is possible, for example, when we are interested in the (non)existence of a given execution state or in the collection of information only at some program points. In particular, Java bytecode verification fits these requirements, and the proposed algorithm can be used to develop a Verifier on memory limited embedded systems, e.g. Java cards [5]