Scalable Symbolic Execution

PhD Qualifying Examination


Title: "Scalable Symbolic Execution"

by

Mr. Peisen YAO


Abstract:

Software errors such as program crashes and security vulnerabilities are 
still a widespread plague. A single software flaw is enough to cause 
irreparable damage, and even software that has been in use for decades and 
deployed to millions of users may still contain flaws. Therefore, 
considerable effort has been undertaken to develop tools and methodologies 
to obtain fault-free software, including simulation, software testing, 
program analysis, formal verification and so on.

Static program analysis analyzes program behaviors without running it and 
can be used for detecting common software errors automatically. Symbolic 
execution is a program analysis technique that systematically enumerates 
feasible program executions with efficient constraint solvers, and can 
prioritize executions of interest. However, path explosion-the fact that 
the number of program executions is typically at least exponential in the 
size of the program-hinders the applicability of symbolic execution in the 
real world, where software commonly reaches millions of lines of code.

In this survey, we summarize the development symbolic execution with an 
emphasis on the scalability challenges. We first introduce the basic 
background and terminologies of symbolic execution. We then summarize the 
trade-offs in designing symbolic executors and present several main 
scalability challenges. After that, we survey related work in addressing 
these challenges in details. At the end, we conclude with some future 
directions for making symbolic execution scalable.


Date:			Monday, 29 January 2018

Time:                  	10:30am - 12:30pm

Venue:                  Room 3494
                         Lifts 25/26

Committee Members:	Dr. Charles Zhang (Supervisor)
 			Prof. Shing-Chi Cheung (Chairperson)
 			Prof. Fangzhen Lin
 			Dr. Wei Wang


**** ALL are Welcome ****