It’s often very challenging for programmers to understand the semantics of concurrent code. The goal of our project is to verify the DRF properties for the Weakestmo memory model. For a programmer, it means that avoiding data races weaker than SC (or any data races) in his/her code is enough to rule out all the undesirable weak behaviors. Thus, one can abstract from the weak memory effects and reason as if it were sequentially consistent.