Modern multicore processors provide weak memory models. These memory models seemingly reorder program operations. Thus, they deviate from the commonly assumed sequential consistency (SC) semantics. Verification techniques for concurrent programs consequently need to take these weak semantics into account. Linearizability, a de-facto standard correctness condition for concurrent data structures, has been defined under assumption of SC and its meaning under weak memory models was uncertain for years. Just recently, new adaptations were proposed. We present a verification approach for concurrent programs under the weak memory models TSO and PSO. The approach is based on a reduction of concurrent programs under TSO (resp. PSO) to an SC program enabling many standard SC verification tools. The reduction involves two steps: a symbolic exploration, which results in a representation of the program behavior under TSO (resp. PSO) as a store buffer graph. The latter is then transformed into a new SC program. We prove both programs to be behaviorally equivalent (bisimulation). Our tool Weak2SC implements the presented approach. Furthermore, we evaluate our reduction approach by comparing it against more common explicit models of weak memory semantics. We take existing approaches for verification of linearizability under SC and adapt them for weak memory models. We apply these approaches to a set of typical concurrent data structures and achieve promising results in terms of performance (resp. proof effort). In addition, we also discuss how the adapted verification approaches relate to the new formalizations of linearizability under weak memory models.