Assertion guided symbolic execution of multithreaded programs

Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

45 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publication2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015 - Proceedings
PublisherAssociation for Computing Machinery, Inc
Pages854-865
Number of pages12
ISBN (Electronic)9781450336758
DOIs
StatePublished - Aug 30 2015
Event10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015 - Bergamo, Italy
Duration: Aug 30 2015Sep 4 2015

Publication series

Name2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015 - Proceedings

Other

Other10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2015
Country/TerritoryItaly
CityBergamo
Period8/30/159/4/15

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Concurrency
  • Partial order reduction
  • Symbolic execution
  • Test generation
  • Weakest precondition

Fingerprint

Dive into the research topics of 'Assertion guided symbolic execution of multithreaded programs'. Together they form a unique fingerprint.

Cite this