Parallelizing Path Exploration and Optimizing Constraint Solving for Efficient Symbolic Execution
Date
2020-10
Authors
Wen, Junye
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Symbolic execution executes programs with symbolic inputs and systematically analyzes program behaviors by exploring all feasible paths. For each path it explores, it builds a path condition, and checks the path's feasibility by solving its corresponding path condition using off-the-shelf constraint solvers. Symbolic execution is a powerful program analysis technique and has provided a basis for various software testing and verification techniques. However, it remains expensive and is difficult to be applied for large and complex programs due to two major challenges: (1) path explosion problem, i.e., the number of feasible paths in a program grows exponentially with an increase in program size, and (2) constraint solving is expensive.
This dissertation presents four techniques for efficient symbolic execution. The first two techniques, STAPAR and STASE, address the problem of path explosion by parallelizing path exploration in the context of checking properties using symbolic execution. STAPAR statically partitions a check for the whole set of properties into multiple simpler sub-checks, so that different properties are checked in parallel. STASE runs two stages in parallel: one stage for locating all feasible paths to properties and the other stage for checking properties along these paths in parallel. The other two techniques, DeepSolver and Cocoa, optimize constraint solving to improve its efficiency. DeepSolver trains deep neural networks using existing constraint solutions, and uses the trained deep neural networks to classify path conditions for their satisfiability. Cocoa reduces the complexity of path conditions by replacing unimportant symbolic variables with concrete values. Experimental evaluations have shown the efficacy of our techniques compared to the state-of-the-art techniques.
Description
Keywords
Symbolic execution, Parallel processing, Deep learning
Citation
Wen, J. (2020). Parallelizing path exploration and optimizing constraint solving for efficient symbolic execution</i> (Unpublished dissertation). Texas State University, San Marcos, Texas.