TY - GEN
T1 - Assertion guided symbolic execution of multithreaded programs
AU - Guo, Shengjian
AU - Kusano, Markus
AU - Wang, Chao
AU - Yang, Zijiang
AU - Gupta, Aarti
N1 - Funding Information:
This work was primarily supported by the NSF under grants CCF-1149454, CCF-1405697, and CCF-1500024. Partial support was provided by the ONR under grant N00014-13-1-0527. Any opinions, findings, and conclusions expressed in this material are those of the authors and do not necessarily reflect the views of the funding agencies.
Publisher Copyright:
© 2015 ACM.
PY - 2015/8/30
Y1 - 2015/8/30
N2 - 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.
AB - 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.
KW - Concurrency
KW - Partial order reduction
KW - Symbolic execution
KW - Test generation
KW - Weakest precondition
UR - http://www.scopus.com/inward/record.url?scp=84960389950&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84960389950&partnerID=8YFLogxK
U2 - 10.1145/2786805.2786841
DO - 10.1145/2786805.2786841
M3 - Conference contribution
AN - SCOPUS:84960389950
T3 - 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
SP - 854
EP - 865
BT - 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
PB - Association for Computing Machinery, Inc
T2 - 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015
Y2 - 30 August 2015 through 4 September 2015
ER -