Parameterized Model Checking Modulo Explicitweak Memory Models
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE(2018)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络