We consider concurrent programs composed of a fixed number of threads over an infinite data domain. The verification of such concurrent programs requires finite state abstractions expressed through Floyd/Hoare-style assertions and it raises the problem of interleavings: each order in which the system may schedule threads has to be considered. Automatic abstraction refinement gives us techniques to find Floyd/Hoare-style assertions in software model checking. In this paper, we present a method of abstraction refinement which, given a verification problem for a concurrent program, constructs a model checking problem for a Petri net. The idea is to translate Floyd/Hoare-style assertions into synchronization constraints; by adding synchronization constraints to the Petri net, we refine the abstraction of the concurrent program through the Petri net. We solve the Petri net model checking problem via McMillan’s unfoldings which allows us to handle the large number of interleavings.