A new simulation algorithm for inter-procedural, context-sensitive, and path-sensitive value flow analysis is described in this paper. Value flow analysis investigates which memory locations hold a given value; it is used in software validation tools. The challenge for these tools is the development of practical algorithms for large programs. The authors apply known results for memory aliasing and path merging, with implicit representation of value sets, to produce a practical algorithm, which they demonstrate using a software validation tool, ESP.

The topic of the paper is largely formal, but the authors do a good job of giving examples, and providing insight, appropriate repetition, and explanation. The formal part of the paper consists of a pointer assignment language, definitions of value alias sets and transfer functions, and pseudocode for computing the transfer function to obtain the value alias set for a variable created at a given point in a program. The transfer function is defined in terms of “must” and “may” sets. By varying the definition of these sets, the function calculation can trade-off between accuracy and scalability: a larger “must” set corresponds to more accuracy, and a smaller “may” set, to scalability. No formal definition of the transfer function’s action on states was provided, except indirectly in the pseudocode.

The authors briefly summarize related work, and provide references. Results of applying the algorithm to the Windows kernel are given, but comparisons with alternatives are not provided. The paper is of interest to software engineers working on software validation tools and program analysis.