1. A method for determining whether a program satisfies a safety specification, wherein said program employs a relaxed memory model, said method comprising: obtaining an abstract memory model of said relaxed memory model, wherein said abstract memory model represents concrete program states of said program as a finite number of abstract states; and evaluating said safety specification for said program on said abstract memory model having said finite number of abstract states.