THESIS
2021
1 online resource (ix, 37 pages) : illustrations (some color)
Abstract
Constraints solving takes a large proportion of time in symbolic execution. Z3 Solver
[5], the state-of-the-art tool, specializes in constraint solving and can solve constraints
with customized strategies. The performance of Z3 Solver varies for different groups
of constraints, and a well-performed strategy for a specific group does not convey the
consistent performance for other groups. Numerous approaches address the acceleration
issue (Proteus [13], ISAC [17], SUNNY [3], StartEvo [24]) by inventing algorithms or
learning to choose a well-performed strategy. We rephrase the acceleration problem into
a search space coverage problem. Besides, we extend the coverage of the search space
by embedding reinforcement learning with a natural language processing model. We
evaluate our framework...[
Read more ]
Constraints solving takes a large proportion of time in symbolic execution. Z3 Solver
[5], the state-of-the-art tool, specializes in constraint solving and can solve constraints
with customized strategies. The performance of Z3 Solver varies for different groups
of constraints, and a well-performed strategy for a specific group does not convey the
consistent performance for other groups. Numerous approaches address the acceleration
issue (Proteus [13], ISAC [17], SUNNY [3], StartEvo [24]) by inventing algorithms or
learning to choose a well-performed strategy. We rephrase the acceleration problem into
a search space coverage problem. Besides, we extend the coverage of the search space
by embedding reinforcement learning with a natural language processing model. We
evaluate our framework on ten open source projects from Github. We have obtained a
positive result: our framework has improved the search space coverage and accelerated
Z3 Solver with a lower bound of six times.
Post a Comment