Cubicle-W: Parameterized Model Checking on Weak Memory

被引：5

作者：

Conchon, Sylvain ^{[1
,2
,3
]}

Declerck, David ^{[1
,2
,3
]}

Zaidi, Fatiha ^{[1
,2
]}

机构：

[1] Univ Paris Saclay, CNRS, LRI, F-91405 Orsay, France

[2] Univ Paris Saclay, Univ Paris Sud, F-91405 Orsay, France

[3] Univ Paris Saclay, INRIA, F-91120 Palaiseau, France

来源：

AUTOMATED REASONING, IJCAR 2018 | 2018年 / 10900卷

关键词：

Parameterized model checking; MCMT; SMT; Weak memory; VERIFICATION;

D O I：

10.1007/978-3-319-94205-6_11

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present Cubicle-W, a new version of the Cubicle model checker to verify parameterized systems under weak memory models. Its main originality is to implement a backward reachability algorithm modulo weak memory reasoning using SMT. Our experiments show that Cubicle-W is expressive and efficient enough to automatically prove safety of concurrent algorithms, for an arbitrary number of processes, ranging from mutual exclusion to synchronization barriers.

引用

页码：152 / 160

页数：9

共 21 条

[1] Abdulla P. A, 2016, CONCUR
[2] Abdulla P. A., 2007, TACAS
[3] Abdulla P. A, 2013, TACAS
[4] Abdulla PA, 2007, LECT NOTES COMPUT SC, V4590, P145
[5] Alglave J, 2014, ACM TPLS
[6] Alglave J, 2013, LECT NOTES COMPUT SC, V7792, P512, DOI 10.1007/978-3-642-37036-6_28
[7] Alglave Jade, 2008, P 4 WORKSHOP DECLARA
[8] [Anonymous], 2008, ART MULTIPROCESSOR P
[9] [Anonymous], CACM
[10] LIMITS FOR AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS
APT, KR
KOZEN, DC
[J]. INFORMATION PROCESSING LETTERS, 1986, 22 (06) : 307 - 309

← 1 2 3 →