Advantageous State Merging During Symbolic Analysis

摘要

A determination is made regarding whether to merge two symbolic analysis states. A first state corresponds to a first path through a program to a program location and a second state corresponds to a second path through the program to the program location. A set of variables of the program at the program location is determined. For each variable in the set: a) a first value of the variable in the first state is determined; b) a second value of the variable in the second state is determined; and c) a determination is made, based on the first and second values, regarding whether merging the first and second states would be advantageous. A determination is made, responsive to determining that merging the first state and the second state would not be advantageous for at least one variable in the set, not to merge the first state and the second state.