Parallelizing Path Exploration and Optimizing Constraint Solving for Efficient Symbolic Execution

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.

Name thesis:degree_name

Doctor of Philosophy

Level thesis:degree_level

Doctoral

Discipline thesis:degree_discipline

Computer Science

Grantor

Texas State University

Year dc:date.issued

2020

Author dc:creator

• Wen, Junye

Advisor dc:contributor.advisor

• Yang, Guowei

Committee members dc:contributor.committeemember

• Ngu, Anne H.H.
• Yan, Yan
• Wang, Xiaoyin

• symbolic execution
• parallel processing
• deep learning

Language dc:language.iso

en

Handle dc:identifier.uri

https://hdl.handle.net/10877/12836

OAI identifier oai:identifier

oai:digital.library.txst.edu:10877/12836