1. A computer implemented method for identifying concurrency errors in a concurrent software program comprising the steps of: constructing an initial concurrent trace model (CTM) from an observed concurrent event trace of the concurrent software program; obtaining a set of independent transactions and a set of ordered pairs between the independent transactions by performing a mutually atomic transaction (MAT) analysis on the CTM; identifying specific scenarios of errors that may correspond to concurrency errors; generating a transaction interaction model for each of the scenarios identified; encoding violation conditions for each of the scenarios and generating a quantifier-free satisfiability modulo theory (SMT) formula including the encoded violation conditions; determining any feasible interleaving meeting one or more violation conditions through the effect of a SMT solver on the SMT formula; and outputting any indicia of the interleaving.