CONSTRAINT-SPECIFIC ACCELERATION OF Z3SOLVER WITH EXTENDED SEARCH SPACE COVERAGE

MPhil Thesis Defence


Title: "CONSTRAINT-SPECIFIC ACCELERATION OF Z3SOLVER WITH EXTENDED SEARCH SPACE 
COVERAGE"

By

Mr. Linjie HUANG


Abstract

Constraint solving takes a large proportion of time in symbolic execution. 
Z3 Solver, 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, ISAC, SUNNY, StartEvo) 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.


Date:  			Tuesday, 1 June 2021

Time:			2:00pm - 4:00pm

Zoom meeting: 
https://hkust.zoom.us/j/7373258683?pwd=bEZuQW5KVUx5d3M2aWh5ZHl6N2xwQT09

Committee Members:	Dr. Charles Zhang (Supervisor)
 			Prof. Shing-Chi Cheung (Chairperson)
 			Prof. Raymond Wong


**** ALL are Welcome ****