Survey of the path explosion problem in symbolic execution

PhD Qualifying Examination


Title: "Survey of the path explosion problem in symbolic execution"

by

Mr. Yiyuan GUO


Abstract:

Symbolic execution is a formal method to reason about the properties of an 
execution path of the program and has been widely used in software testing 
and vulnerability detection. It runs the application under test with 
symbolic inputs and forks execution states at conditional branches. The 
symbolic execution engine will use a backend constraint solver to decide 
path feasibility and systematically explore the path space of the program 
according to some searching strategies. Compared to testing, symbolic 
execution can increase the code coverage and thus explore more interesting 
program behaviors.

Even with four decades of research, symbolic execution techniques still 
suffer from the scalability problem to be widely used in testing 
real-world programs. One of the major obstacles is the path explosion 
problem: the number of possible program execution paths grows 
exponentially with the size of the program. In this survey, we investigate 
symbolic execution techniques to alleviate the path explosion problem. 
Depending on the granularity of analysis, some of these techniques operate 
on a single path while others reason about multiple paths. The former 
tries to apply searching heuristics to prioritize over the promising paths 
and sound program analysis techniques to reduce the path space. The latter 
exploits the program structure and effectively group multiple paths 
together and reason them at the same time. We will discuss the details of 
these techniques and their limitations.

After a survey on existing solutions, we will summarize and highlight 
challenges that remain and discuss possible future directions to advance 
towards scalable symbolic execution of real-world programs.


Date:			Friday, 3 July 2020

Time:                  	10:00am - 12:00noon

Zoom meeting:           https://hkust.zoom.us/j/6394211317

Committee Members:	Dr. Charles Zhang (Supervisor)
 			Dr. Dimitrios Papadopoulos (Chairperson)
 			Prof. Cunsheng Ding
 			Dr. Wei Wang


**** ALL are Welcome ****