proceeding Papers Definite Expression Aliasing Analysis for Java Bytecode


We define a novel static analysis for Java bytecode, called definite expression aliasing. It infers, for each variable v at each program point p, a set of expressions whose value at p is equal to the value of v at p, for every possible execution of the program. Namely, it determines which expressions must be aliased to local variables and stack elements of the Java Virtual Machine. This is a useful piece of information for a static analyzer, such as Julia, since it can be used to refine other analyses at conditional statements or assignments. We formalize and implement a constraint-based analysis, defined and proved correct in the abstract interpretation framework. Moreover, we show the benefits of our definite expression aliasing analysis for nullness and termination analysis with Julia.

Paper Details


D. Nikolic,  F. Spoto


The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012), 7521, , 74-89