基于显式弱内存模型的参数化模型检验模理论
计算机科学中的逻辑
2018-05-16 v1
摘要
我们提出了一个模块化框架，用于对具有显式弱内存访问操作的参数化基于数组的迁移系统进行模型检验。我们的方法将 Ghilardi 和 Ranise 的 MCMT（Model Checking Modulo Theories，模型检验模理论）框架扩展为显式弱内存模型。我们在 Cubicle-W（Cubicle 模型检验器的扩展）中实现了这一新框架。我们工具的模块化架构允许我们无缝切换底层内存模型（TSO、PSO……）。我们使用类 TSO 内存模型的初步实验看起来很有前景。
引用
@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}
}
备注
In Proceedings IMPEX 2017 and FM&MDD 2017, arXiv:1805.04636