Directed Model Checking for Fast Abstract Reachability Analysis

被引：0

作者：

Lee, Nakwon ^{[1
]}

Kim, Yunho ^{[2
]}

Kim, Moonzoo ^{[1
]}

Ryu, Duksan ^{[3
]}

Baik, Jongmoon ^{[1
]}

机构：

[1] Korea Adv Inst Sci & Technol, Sch Comp, Daejeon 34141, South Korea

[2] Hanyang Univ, Dept Comp Sci, Seoul 04763, South Korea

[3] Jeonbuk Natl Univ, Dept Software Engn, Jeonju Si 54896, Jeollabuk Do, South Korea

来源：

IEEE ACCESS | 2021年 / 9卷

基金：

新加坡国家研究基金会;

关键词：

Measurement; Runtime; Model checking; Computer bugs; Annotations; Software; Reachability analysis; Software verification; software testing; symbolic model checking; abstract reachability; interprocedural analysis; directed search;

D O I：

10.1109/ACCESS.2021.3130569

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We propose a novel technique (TOUR) to improve both bug detection ability and verification speed of ARMC by detecting a target path quickly. The key idea of TOUR is an error location directed search that utilizes the distance to an error location and function call context at runtime. TOUR applies four different distance metrics and a distance metric selection heuristic using static features of a target program. We have extensively evaluated TOUR on 3,042 real-world C programs in a software verification competition benchmark. The experiment results show that TOUR, due to its error location directed search, finds bugs in 20% more programs in 11% less model checking time than the state-of-the-art ARMC technique (i.e., block-abstraction memoization) for 354 buggy programs. Also, TOUR verifies 15% more programs within 15% less model checking time than the block-abstraction memoization for 652 complex clean programs.

引用

页码：158738 / 158750

页数：13

共 47 条

[1]

Albarghouthi Aws, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P672, DOI 10.1007/978-3-642-31424-7_48

[2]

Albarghouthi A, 2012, LECT NOTES COMPUT SC, V7214, P157, DOI 10.1007/978-3-642-28756-5_12

[3] CPA-BAM-Slicing: Block-Abstraction Memoization and Slicing with Region-Based Dependency Analysis [J].

Andrianov, Pavel ;

Mutilin, Vadim ;

Mandrykin, Mikhail ;

Vasilyev, Anton .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT II, 2018, 10806 :427-431

[4]

[Anonymous], 2019, RPART

[5] Automatic predicate abstraction of C programs [J].

Ball, T ;

Millstein, T ;

Majumdar, R ;

Rajamani, SK .

ACM SIGPLAN NOTICES, 2001, 36 (05) :203-213

[6] A Decade of Software Model Checking with SLAM [J].

Ball, Thomas ;

Levin, Vladimir ;

Rajamani, Sriram K. .

COMMUNICATIONS OF THE ACM, 2011, 54 (07) :68-76

[7]

Beyer Dirk, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P184, DOI 10.1007/978-3-642-22110-1_16

[8] The software model checker BlastApplications to software engineering [J].

Dirk Beyer ;

Thomas A. Henzinger ;

Ranjit Jhala ;

Rupak Majumdar .

International Journal on Software Tools for Technology Transfer, 2007, 9 (5-6) :505-525

[9]

Beyer Dirk, 2012, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies. Proceedings of the 5th International Symposium, ISoLA 2012, P1, DOI 10.1007/978-3-642-34032-1_1

[10]

Beyer D., 2010, 2010 Formal Methods in Computer-Aided Design (FMCAD 2010), P189

← 1 2 3 4 5 →