1. A method for program verification by 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 an amount of memory needed to verify the program and a number of steps taken to uncover an error.