Assertion Guided Symbolic Execution of Multithreaded Programs

被引：38

作者：

Guo, Shengjian ^{[1
]}

Kusano, Markus ^{[1
]}

Wang, Chao ^{[1
]}

Yang, Zijiang ^{[2
]}

Gupta, Aarti ^{[3
]}

机构：

[1] Virginia Tech, Blacksburg, VA 24061 USA

[2] Western Michigan Univ, Kalamazoo, MI 49008 USA

[3] Princeton Univ, Princeton, NJ 08544 USA

来源：

2015 10TH JOINT MEETING OF THE EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND THE ACM SIGSOFT SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE 2015) PROCEEDINGS | 2015年

基金：

美国国家科学基金会;

关键词：

Symbolic execution; test generation; concurrency; partial order reduction; weakest precondition;

D O I：

10.1145/2786805.2786841

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Symbolic execution is a powerful technique for systematic testing of sequential and multithreaded programs. However, its application is limited by the high cost of covering all feasible intra-thread paths and inter-thread interleavings. We propose a new assertion guided pruning framework that identifies executions guaranteed not to lead to an error and removes them during symbolic execution. By summarizing the reasons why previously explored executions cannot reach an error and using the information to prune redundant executions in the future, we can soundly reduce the search space. We also use static concurrent program slicing and heuristic minimization of symbolic constraints to further reduce the computational overhead. We have implemented our method in the Cloud9 symbolic execution tool and evaluated it on a large set of multithreaded C/C++ programs. Our experiments show that the new method can reduce the overall computational cost significantly.

引用

页码：854 / 865

页数：12

共 59 条

[1] Abdulla Parosh Aziz, 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, P353, DOI 10.1007/978-3-662-46681-0_28
[2] ADVE V, 2003, ACM IEEE INT S MICR
[3] Andersen L. O., 1994, Technical Report
[4] [Anonymous], 2014, IEEE ACM INT C AUT S, DOI DOI 10.1145/2642937.2642998
[5] [Anonymous], 1976, A discipline of programming
[6] [Anonymous], 1996, LECT NOTES COMPUTER, DOI DOI 10.1007/3-540-60761-7
[7] Ball T., 2004, Formal Methods for Components and Objects. Third International Symposium, FMCO 2004. Revised Lectures (Lecture Notes in Computer Science Vol. 3657), P1
[8] Bergan T, 2014, ACM SIGPLAN NOTICES, V49, P491, DOI [10.1145/2660193.2660200, 10.1145/2714064.2660200]
[9] Beyer D, 2012, PROCEEDINGS OF THE 12TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2012), P106
[10] Boonstoppel P, 2008, LECT NOTES COMPUT SC, V4963, P351, DOI 10.1007/978-3-540-78800-3_27

← 1 2 3 4 5 6 →