Distributed Symbolic Execution For Property Checking
Date
2017-05
Authors
Wen, Junye
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Symbolic execution is a powerful technique for checking properties in the form of assertions. It can systematically explore the program’s state space to find paths to assertion violations, and provide users with a counterexample for each violation by solving the corresponding path condition using the underlying constraint solver. However, conventional symbolic execution is configured either to explore all the state space to find all possible assertion violations, or to stop when it finds the first assertion violation. In the former case, one symbolic execution run could take a long time before giving any result, and users have to wait for the whole execution time before they could take any action to deal with the potential problems in their code. In the latter case, users need to run symbolic execution for multiple times to check all assertion violations.
In this thesis, we develop a novel technique to check assertions in parallel using symbolic execution. Our technique improves the efficiency of assertion checking using symbolic execution and gives users earlier results. This technique is in two stages: in the first stage, a worker is launched to find feasible paths to the checked assertions, then in the second stage, multiple workers are launched to check assertions on these paths in parallel simultaneously, each worker focusing on one of these feasible paths. We evaluate our technique using experiments with four Java subjects, and the experimental results show its effectiveness and efficiency.
Description
Keywords
Symbolic execution, Property checking, Parallel algorithm
Citation
Wen, Ju. (2017). <i>Distributed symbolic execution for property checking</i> (Unpublished thesis). Texas State University, San Marcos, Texas.