Author: Deng Xianghua
Publisher: Springer Publishing Company
ISSN: 0928-8910
Source: Automated Software Engineering, Vol.19, Iss.3, 2012-09, pp. : 233-301
Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.
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.
Related content
Formal specification of parallel SIMD execution
By Farrell C.A. Kieronska D.H.
Theoretical Computer Science, Vol. 169, Iss. 1, 1996-11 ,pp. :