Verifying concurrent programs under weak memory models / vorgelegt von Oleg Travkin, M.Sc.