Parameterized Model Checking Modulo Explicit Weak Memory Models

Sylvain Conchon, David Declerck, Fatiha Zaïdi

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…