Efficient and formal generalized symbolic execution

K-REx Repository

Show simple item record

dc.contributor.author Deng, Xianghua
dc.contributor.author Lee, Jooyong
dc.contributor.author Robby
dc.date.accessioned 2012-11-12T16:51:52Z
dc.date.available 2012-11-12T16:51:52Z
dc.date.issued 2012-11-12
dc.identifier.uri http://hdl.handle.net/2097/14930
dc.description.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. en_US
dc.language.iso en_US en_US
dc.relation.uri http://www.springerlink.com/content/k2wh786791202n43/ en_US
dc.rights The final publication is available at www.springerlink.com en_US
dc.subject Symbolic execution en_US
dc.subject Operational semantics en_US
dc.subject JVM en_US
dc.subject Soundness en_US
dc.subject Completeness en_US
dc.title Efficient and formal generalized symbolic execution en_US
dc.type Article (author version) en_US
dc.date.published 2012 en_US
dc.citation.doi doi:10.1007/s10515-011-0089-9 en_US
dc.citation.epage 301 en_US
dc.citation.issue 3 en_US
dc.citation.jtitle Automated Software Engineering en_US
dc.citation.spage 233 en_US
dc.citation.volume 19 en_US
dc.contributor.authoreid robby en_US

Files in this item


Files Size Format View

This item appears in the following Collection(s)

Show simple item record