View in EDS

Conditional termination of loops over heap-allocated data.

Saved in:
Bibliographic Details
Title: Conditional termination of loops over heap-allocated data.
Authors: Albert, Elvira1 elvira@sip.ucm.es, Arenas, Puri1 puri@sip.ucm.es, Genaim, Samir1 samir@fdi.ucm.es, Puebla, Germán2 german@fi.upm.es, Román-Díez, Guillermo2 groman@fi.upm.es
Source: Science of Computer Programming. Oct2014, Vol. 92 Issue Part A, p2-24. 23p.
Subjects: Computer software termination, Data analysis, Computational complexity, Information retrieval, Java programming language, Mathematical proofs
Abstract: Abstract: Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in Java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable. [Copyright &y& Elsevier]
Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:Abstract: Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in Java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable. [Copyright &y& Elsevier]
ISSN:01676423
DOI:10.1016/j.scico.2013.04.006