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 [J].

APT, KR ;

KOZEN, DC .

INFORMATION PROCESSING LETTERS, 1986, 22 (06) :307-309

← 1 2 3 →