A simple abstraction of arrays and maps by program translation

David Monniaux, Francesco Alberti

We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar opera…