Patent ID: 6938186

Claim:
A method for performing path-sensitive verification on a software program, the method comprising: traversing a logic path in the software program, the logic path having a plurality of nodes, each of the plurality of nodes having at least one edge associated therewith, the at least one edge linking a first node and a second node out of the plurality of nodes; maintaining a symbolic store associated with a property being tested, the symbolic store including a plurality of symbolic states, each symbolic state having an abstract state and a concrete state, the abstract state identifying a current property state out of a plurality of property states for the property being tested and the concrete state identifying current information associated with other properties in the software program, each symbolic state being associated with one edge; traversing a current path in the logic path using a current symbolic state out of the plurality of symbolic states, the current path including a current node out of the plurality of nodes and a current edge that is associated with the current node; and updating the symbolic store to reflect changes in the abstract state and in the concrete state based on the current path, wherein the symbolic store is updated in a manner such that no two symbolic states associated with the current edge have identical abstract states.