Show simple item record

dc.contributor.advisorYang, Guowei
dc.contributor.authorWen, Junye ( )
dc.identifier.citationWen, J. (2020). Parallelizing path exploration and optimizing constraint solving for efficient symbolic execution (Unpublished dissertation). Texas State University, San Marcos, Texas.

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.

dc.format.extent148 pages
dc.format.medium1 file (.pdf)
dc.subjectSymbolic execution
dc.subjectParallel processing
dc.subjectDeep learning
dc.subject.lcshSoftware engineering
dc.subject.lcshParallel programming (Computer science)
dc.titleParallelizing Path Exploration and Optimizing Constraint Solving for Efficient Symbolic Execution
dc.contributor.committeeMemberNgu, Anne H. H.
dc.contributor.committeeMemberYan, Yan
dc.contributor.committeeMemberWang, Xiaoyin Science Science State University of Philosophy
dc.description.departmentComputer Science



This item appears in the following Collection(s)

Show simple item record