Parameterized Model Checking Modulo Explicit Weak Memory Models
Logic in Computer Science
2018-05-16 v1
Abstract
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 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.
Cite
@article{arxiv.1805.05515,
title = {Parameterized Model Checking Modulo Explicit Weak Memory Models},
author = {Sylvain Conchon and David Declerck and Fatiha Zaïdi},
journal= {arXiv preprint arXiv:1805.05515},
year = {2018}
}
Comments
In Proceedings IMPEX 2017 and FM&MDD 2017, arXiv:1805.04636