Title
Conditional termination of loops over heap-allocated data.
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.
Year
DOI
Venue
2014
10.1016/j.scico.2013.04.006
Science of Computer Programming
Keywords
Field
DocType
Static analysis,Heap-sensitive analysis,Termination,Java bytecode,Program transformation
Locality,Programming language,Program transformation,Computer science,Static analysis,Heap (data structure),Java bytecode,Software,Bytecode,Java
Journal
Volume
ISSN
Citations 
92
0167-6423
4
PageRank 
References 
Authors
0.40
26
5
Name
Order
Citations
PageRank
Elvira Albert1110068.19
P. Arenas21174.80
Samir Genaim389144.31
Germán Puebla4147876.38
Guillermo Román-Díez5938.92