Show simple item record

dc.contributor.advisorYang, Guowei
dc.contributor.authorWen, Junye ( )
dc.date.accessioned2020-10-26T14:21:59Z
dc.date.available2020-10-26T14:21:59Z
dc.date.issued2020-10
dc.identifier.citationWen, J. (2020). Parallelizing path exploration and optimizing constraint solving for efficient symbolic execution (Unpublished dissertation). Texas State University, San Marcos, Texas.
dc.identifier.urihttps://digital.library.txstate.edu/handle/10877/12836
dc.description.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.

dc.formatText
dc.format.extent148 pages
dc.format.medium1 file (.pdf)
dc.language.isoen
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
txstate.documenttypeDissertation
dc.contributor.committeeMemberNgu, Anne H. H.
dc.contributor.committeeMemberYan, Yan
dc.contributor.committeeMemberWang, Xiaoyin
thesis.degree.departmentComputer Science
thesis.degree.disciplineComputer Science
thesis.degree.grantorTexas State University
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy
dc.description.departmentComputer Science


Download

Thumbnail

This item appears in the following Collection(s)

Show simple item record