Patent ID: 8176496

Claim:
A method for conducting symbolic partial order reduction for concurrent systems of multithreaded executions, comprising: determining a guarded independence relation which includes transitions from different threads that are independent for a set of states, when a condition or predicate holds; performing symbolic partial order reduction in bounded model checking using the guarded independence relation to permit automatic pruning of redundant thread interleavings when the guarded independence condition holds; and representing all possible length-k interleavings by adding at every time frame copies of program state variables with Φ := I ⁡ ( V 0 ) ⋀ ⋀ i = 0 k ⁢ ( SCH ⁡ ( V i ) ⋀ ⋀ j = 1 N ⁢ TR j ⁡ ( V i , V i + 1 ) ) , where v i εV i denotes a copy of vεV at the i-th time frame and I(v 0 ) represents a set of initial states, SCH represents a transition relation of a scheduler, and TR j ; represents the transition of thread T j .