Symbolic reduction of dynamic executions of concurrent programs

1. A method for determining the correctness of a concurrent software program, said method comprising the computer implemented steps of:

partitioning the concurrent software program into a number of concurrent trace programs (CTPs);

applying a satisfiability method (SAT) to each of the CTPs in isolation;

determining whether a property violation occurs within the CTP as a result of the SAT;

determining whether the CTP is redundant with respect to the property; and

outputting an indicia of the determination.

2. The method of claim 1 further comprising the computer implemented steps of:

generating a set of concrete traces from which the CTPs are determined.

3. The method of claim 2 further comprising the steps of:

evaluating, using the SAT method, all feasible executions of the CTPs.

4. The method of claim 2 further comprising the steps of:

generating an abstraction of the CTPs; and

determining using the SAT method, an indication of whether the abstraction is error free.

5. The method of claim 4 further comprising the steps of:

identifying, using the abstraction determination, whether other CTPs are redundant with respect to the property.

6. The computer implemented method of claim 1 operating in a stateless dynamic model checking system.

7. The method of claim 3 wherein the SAT method uses an efficient symbolic encoding based on a Concurrent Static Single Assignment (CSSA) form.

8. The method of claim 1 wherein said concurrent trace program CTP ρ is a partially ordered set (T, ), where T={t|t is an event in ρ}, and is the partial order such that, for two arbitrary events t i , t j ∈T, we have t i t j iff i=j, or one of the following conditions holds:

tid(t i )=tid(t j ) and i<j in ρ,

tid(t i )≠tid(t j ) and there exist t k , t i ∈T such that t i t k , t i t j , and

either t k has action fork(tid(t l )), or t l has action join(tid(t k ));

wherein ρ is an execution trace of the concurrent software program.

9. A computer implemented method for determining the correctness of a concurrent software program using dynamic model checking, said method comprising the computer implemented steps of:

determining a set of concrete executions for the software program;

partitioning the software program into a set of concurrent trace programs (CTPs) determined from the set of concrete executions;

checking each CTP for errors in isolation through the effect of a satisfiability analysis (SAT);

pruning redundant CTPs from the set of CTPs;

outputting an indicia of the correctness of the CTPs.

10. The method of claim 9 wherein said concurrent trace program CTP ρ is a partially ordered set(T, ), where T={t|t is an event in ρ}, and is the partial order such that, for two arbitrary events t i , t j ∈T, we have t i t j iff i=j, or one of the following conditions holds:

tid(t i )=tid(t j ) and i<j in ρ,

tid(t i )≠tid(t j ) and there exist t k , t l ∈T such that t i t k , t l t j , and

either t k has action fork(tid(t l ), or t l has action join(tid(t k ));

wherein ρ is an execution trace of the concurrent software program.