Described is a method and system that performs path-sensitive verification
on programs having any code base size. The method maintains a symbolic store that
includes symbolic states. Each symbolic state includes a concrete state and an
abstract state. The abstract state identifies a state in which the property being
tested currently exists. The concrete state identifies other properties of the
program. The symbolic store is updated at each node in a logic path of the program
with changes in the abstract state and the concrete state. The updates occur such
that the symbolic states associated with a particular edge of any node will not
have identical abstract states. Rather, in this case, the symbolic states are merged
by combining the concrete states to include content that is similar in both symbolic
states. In addition, the concrete state determines relevant paths to proceed along
in the logic path.