Abstract:The research of precise execution reachability analysis focuses on figuring out the reachability between program states. It tries to find witness inputs and the execution traces that pass through the setting-up target state of certain code location by performing necessary test and verification on executable files, source code and documentation. Precise execution reachability analysis has been applied to direct testing, bug reproduction, construction of proof of concepts of vulnerabilities, verification for result of static analysis and so on. This paper provides a survey of this area. First, the corresponding constraint solving problem of precise reachability analysis is cited. Next, existing typical methods and technical difficulties about bidirectional symbolic analysis and program induction, and some technical difficulties are discussed. Then, the applications of current precise reachability analysis are classified and summarized. Furthermore, the challenges on program analysis, program induction and constraint solving are provided. Last but not least, the possible solution and future research are suggested.