RT Journal Article
T1 Conditional Termination of Loops over Heap-Allocated Data
A1 Albert Albiol, Elvira María
A1 Arenas Sánchez, Purificación
A1 Genaim, Samir
A1 Puebla, Germán
A1 Román Díez, Guillermo
AB 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.
PB Elsevier
SN 0167-6423
YR 2014
FD 2014-10
LK https://hdl.handle.net/20.500.14352/35134
UL https://hdl.handle.net/20.500.14352/35134
LA eng
NO Unión Europea. FP7
NO Comunidad de Madrid
NO Ministerio de Ciencia e Innovación (MICINN)
NO UCM-BSCH-GR35/10-A-910502 grant
DS Docta Complutense
RD 17 abr 2025