Parameterized Model Checking Modulo Explicitweak Memory Models

We present a modular framework for model checking parameterized array-based transition systems with explicit access operations on weak memory. Our approach extends the MCMT (Model Checking Modulo Theories) framework of Ghilardi and Ranise [10] with explicit weak memory models. We have implemented this new framework in Cubicle-W, an extension of the Cubicle model checker. The modular architecture of our tool allows us to change the underlying memory model seamlessly (TSO, PSO...). Our first experiments with a TSO-like memory model look promising.