Parameterized Model Checking Modulo Explicit Weak Memory Models

Sylvain Conchon
(Université Paris-Sud)
David Declerck
(Université Paris-Sud)
Fatiha Zaïdi
(Université Paris-Sud)

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.

In Régine Laleau, Dominique Méry, Shin Nakajima and Elena Troubitsyna: Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD) (IMPEX 2017 and FM&MDD 2017), Xi'An, China, 16th November 2017, Electronic Proceedings in Theoretical Computer Science 271, pp. 48–63.
Published: 12th May 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.271.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org