Stateless Model Checking for TSO and PSO

Parosh Abdulla, Stavros Aronis, Mohammed Faouzi Atig +3

We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel represent…