Efficient and formal generalized symbolic execution |
| |
Authors: | Xianghua Deng Jooyong Lee Robby |
| |
Affiliation: | 1.Pennsylvania State University at Harrisburg,Middletown,USA;2.Google Inc.,Mountain View,USA;3.Korea University,Seoul,Korea;4.Kansas State University,Manhattan,USA |
| |
Abstract: | Programs that manipulate dynamic heap objects are difficult to analyze due to issues like aliasing. Lazy initialization algorithm enables the classical symbolic execution to handle such programs. Despite its successes, there are two unresolved issues: (1) inefficiency; (2) lack of formal study. For the inefficiency issue, we have proposed two improved algorithms that give significant analysis time reduction over the original lazy initialization algorithm. In this article, we formalize the lazy initialization algorithm and the improved algorithms as operational semantics of a core subset of the Java Virtual Machine (JVM) instructions, and prove that all algorithms are relatively sound and complete with respect to the JVM concrete semantics. Finally, we conduct a set of extensive experiments that compare the three algorithms and demonstrate the efficiency of the improved algorithms. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|