Context and Precondition-Guided Search Strategies in Dynamic Symbolic Execution

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering


PhD Thesis Defence


Title: "Context and Precondition-Guided Search Strategies in Dynamic 
Symbolic Execution"

By

Mr. Hyunmin Seo


Abstract

Dynamic symbolic execution (DSE) or concolic testing is an automatic test 
input generation technique based on symbolic execution. Due to its low 
false positives and high branch coverages, DSE has received much interest 
both in industry and academia. However, one of the biggest challenges in 
DSE is the path explosion. The number of execution paths increases 
exponentially to the number of branches in a program and exploring all 
paths with DSE becomes infeasible even for a medium sized program. To 
efficiently explore the search space of DSE, we present two search 
strategies. The Context Guided-Search strategy aims to achieve a high 
branch coverage fast. The key idea behind the CGS is to focus on exploring 
diverse states of the program by selecting branches in a new context 
first. We use dominator information to exclude irrelevant branches from 
the context information and incrementally increase the consideration level 
of context. On the other hand, the Precondition Guided-Search strategy 
aims to generate inputs to cover a specific target branch. The PGS 
strategy calculates preconditions for not reaching the target branch from 
previous execution paths which failed to reach the target branch. The PGS 
strategy builds the preconditions in a bottom-up manner with incremental 
merge and uses the preconditions to reduce the search space.
The evaluation results show that the CGS strategy can cover more branches 
than other search strategies on various subjects and the PGS strategy can 
cover the target branch which cannot be covered easily by other 
strategies.


Date:			Wednesday, 28 January 2015

Time:			1:30pm - 3:30pm

Venue:			Room 4472
 			Lifts 25/26

Chairman:		Prof. Christopher Leung (CIVL)

Committee Members:	Prof. Sunghun Kim (Supervisor)
 			Prof. Shing-Chi Cheung
 			Prof. Charles Zhang
 			Prof. Li Qiu (ECE)
 			Prof. Cristian Cadar (Comp., Imperial College London)


**** ALL are Welcome ****