Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation

被引：5

作者：

Nguyen, Truc L. ^{[1
]}

Inverso, Omar ^{[4
]}

Fischer, Bernd ^{[2
]}

La Torre, Salvatore ^{[3
]}

Parlato, Gennaro ^{[1
]}

机构：

[1] Univ Southampton, Elect & Comp Sci, Southampton, Hants, England

[2] Stellenbosch Univ, Div Comp Sci, Stellenbosch, South Africa

[3] Univ Salerno, Dipartimento Informat, Fisciano, Italy

[4] Gran Sasso Sci Inst, Laquila, Italy

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II | 2017年 / 10206卷

基金：

英国工程与自然科学研究理事会;

关键词：

C-PROGRAMS; TOOL;

D O I：

10.1007/978-3-662-54580-5_26

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Lazy sequentialization has emerged as one of the most effective techniques to find bugs in concurrent programs. However, the size of the shared global and thread-local state still poses a problem for further scaling. We therefore use abstract interpretation to minimize the representation of the concurrent program's state variables. More specifically, we run the Frama-C abstract interpretation tool over the sequentialized program output by Lazy-CSeq to compute over-approximating intervals for all (original) state variables and then exploit CBMC's bitvector support to reduce the number of bits required to represent these in the sequentialized program. We demonstrate that this leads to substantial performance gains on complex instances.

引用

页码：375 / 379

页数：5

共 11 条

[1] Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016) [J].

Beyer, Dirk .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016), 2016, 9636 :887-904

[2] A Value Analysis for C programs [J].

Canet, Geraud ;

Cuoq, Pascal ;

Monate, Benjamin .

2009 NINTH IEEE INTERNATIONAL WORKING CONFERENCE ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2009, :123-124

[3] A tool for checking ANSI-C programs [J].

Clarke, E ;

Kroening, D ;

Lerda, F .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 :168-176

[4]

Fischer B, 2013, IEEE INT CONF AUTOM, P710, DOI 10.1109/ASE.2013.6693139

[5] Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-Threaded C-Programs [J].

Inverso, Omar ;

Nguyen, Truc L. ;

Fischer, Bernd ;

La Torre, Salvatore ;

Parlato, Gennaro .

2015 30TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2015, :807-812

[6]

Inverso O, 2014, LECT NOTES COMPUT SC, V8559, P585, DOI 10.1007/978-3-319-08867-9_39

[7]

Inverso Omar, 2014, P LECT NOTES COMPUTE, V8413, P398, DOI [10.1007/ 978- 3- 642- 54862- 8_ 29, DOI 10.1007/978-3-642-54862-8_29]

[8] Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs [J].

Nguyen, Truc L. ;

Fischer, Bernd ;

La Torre, Salvatore ;

Parlato, Gennaro .

AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 :174-191

[9]

Tomasco Ermenegildo, 2015, Tools and Algorithms for the Construction and Analysis of Systems. 21st International Conference, TACAS 2015, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015. Proceedings: LNCS 9035, P551, DOI 10.1007/978-3-662-46681-0_52

[10]

Tomasco E, 2016, PROCEEDINGS OF THE 2016 16TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2016), P193, DOI 10.1109/FMCAD.2016.7886679

← 1 2 →