Inferring complete initialization of arrays

We define an automaton-based abstract interpretation of a trace semantics which identifies loops that definitely initialize all elements of an array to values satisfying a given property, a useful piece of information for the static analysis of Java-like languages. This results in a completely automatic and efficient analysis, that does not use manual code annotations. We give a formal proof of correctness that considers aspects such as side-effects of method calls. We show how the identification of those loops can be lifted to global invariants about the contents of elements of fields of array type, that hold everywhere in the code where those elements are accessed. This makes our work more significant and useful for the static analysis of real programs. The implementation of our analysis inside the Julia analyzer is both efficient and precise.