A Survey of Symbolic Execution and Its Tool KLEE

被引：1

作者：

Zhang, Tao ^{[1
]}

Wang, Pan ^{[2
]}

Guo, Xi ^{[1
]}

机构：

[1] Huazhong Agr Univ, Coll Informat, Dept Comp Sci, Wuhan, Hubei, Peoples R China

[2] Wuhan Elect Power Tech Coll, Dept Power Engn, Wuhan, Hubei, Peoples R China

来源：

PROCEEDINGS OF THE 3RD INTERNATIONAL CONFERENCE ON MECHATRONICS AND INTELLIGENT ROBOTICS (ICMIR-2019) | 2020年 / 166卷

关键词：

Symbolic Execution; KLEE; Test Cases; Path Explosion; Constraint Solving;

D O I：

10.1016/j.procs.2020.02.090

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

Symbolic execution is a highly practical program analysis technology. With the gradual deepening of its research and the continuous maturity of technology itself, it has been widely used in software testing and other fields. KLEE is a symbolic execution tool built on the LLVM compilation framework that automatically generates test cases for high coverage of complex and environmentally intensive programs. This article comprehensively describes the basic principle, development situation, current issues of symbolic execution, and KLEE's infrastructure as well as the generation of test cases. To some extent, it highlights the unique advantages of symbolic execution in software testing and analysis. (C) 2020 The Authors. Published by Elsevier B.V.

引用

页码：330 / 334

页数：5

共 12 条

[1]

Boonstoppel P, 2008, LECT NOTES COMPUT SC, V4963, P351, DOI 10.1007/978-3-540-78800-3_27

[2]

Burnim Jacob, 2008, 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, P443, DOI 10.1109/ASE.2008.69

[3]

Cadar C, 2009, USENIX C OPERATING S, P209

[4]

Cadar C, 2011, 2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), P1066, DOI 10.1145/1985793.1985995

[5] EXE: Automatically Generating Inputs of Death [J].

Cadar, Cristian ;

Ganesh, Vijay ;

Pawlowski, Peter M. ;

Dill, David L. ;

Engler, Dawson R. .

ACM TRANSACTIONS ON INFORMATION AND SYSTEM SECURITY, 2008, 12 (02)

[6]

Dai Zhanying, 2009, RES MEMORY MODEL SYM

[7] DART: Directed automated random testing [J].

Godefroid, P ;

Klarlund, N ;

Sen, K .

ACM SIGPLAN NOTICES, 2005, 40 (06) :213-223

[8]

Kang Wentao, 2014, DESIGN IMPLEMENTATIO

[9] SYMBOLIC EXECUTION AND PROGRAM TESTING [J].

KING, JC .

COMMUNICATIONS OF THE ACM, 1976, 19 (07) :385-394

[10]

Kononov Vasiliy, 2018, PROCEDIA COMPUTER SC

← 1 2 →