Program Representation for Symbolic Analysis
Symbolic analysis is a type of program analysis that can effectively identify semantics of programs. Previous research has shown that it is useful for automatically generating test inputs, detecting bugs, debugging programs and analysing malware. The challenge of symbolic analysis is to make it scalable to large software while still preserving its precision. In this talk, I will first introduce an efficient symbolic analysis, namely segmented demand driven symbolic analysis, that ensure the scalability and precision of the analysis, and I will then present program representations we developed to enable such analysis on solving practical problems, such as verifying software patches and detecting bugs in Android apps.