1. A computer implemented method for program verification by via bounded or unbounded model checking in concurrent programs, comprising: modeling each of a plurality of program threads as a circuit model; generating a full circuit for an entire program by combining the circuit models including constraints which enforce synchronous execution of the program threads; and verifying the program using the synchronous execution to reduce the amount of memory needed to verify the program and a number of steps taken to uncover an error; wherein using the synchronous execution includes determining synchronous conflicts conflicts to determine the subset of transitions that must be explored from each global state.