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.