Skip to main content

Assertion guided symbolic execution of multithreaded programs

Author(s): Guo, Shengjian; Kusano, Markus; Wang, Chao; Yang, Zijiang; Gupta, Aarti

To refer to this page use:
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.
Publication Date: 2015
Citation: Guo, Shengjian, Markus Kusano, Chao Wang, Zijiang Yang, and Aarti Gupta. "Assertion guided symbolic execution of multithreaded programs." In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (2015): pp. 854-865. doi:10.1145/2786805.2786841
DOI: 10.1145/2786805.2786841
Pages: 854 - 865
Type of Material: Conference Article
Journal/Proceeding Title: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.