|Publication Type||Journal Article|
|Year of Publication||2006|
|Authors||Hill PM, Spoto F|
|Journal||Higher-Order and Symbolic Computation|
|Keywords||abstract interpretation, escape analysis, Java, object-oriented languages, software verification, static analysis|
Escape analysis of object-oriented languages determines, for every program point, the creation points of the objects reachable from the variables. This information allows us to stack allocate dynamically created objects and to reduce the overhead of synchronisation in Java-like languages. In this paper, we formalise the escape property E, computed by an escape analysis, as an abstract interpretation of concrete states. We show that it interacts with the static type information and with the late-binding mechanism. A static analysis based on the domain E can only be very imprecise. Therefore, we define a refinement ER of E, in the sense that ER is more concrete than E and, hence, leads to a more precise escape analysis than E. Our implementation of ER is a formally correct escape analyser, able to detect the stack allocatable creation points of middle-size Java (bytecode) applications.