Generic Abstraction of Dictionaries and Arrays

We present a generic abstract domain for analysis of dictionary and array content. Our technique is parametrised by the abstractions of scalars, dictionary keys and dictionary values. It can be instantiated with various existing domains, including non-numerical ones (such as domains for analysis of properties of string variables). It is powerful enough to express relations between container content and scalars.The analysis is fully automatic. The container is partitioned according to properties of the keys, captured by the underlying key abstraction. The precision and cost of the analysis are customisable and depend on the choice of the abstractions of keys, dictionary elements and scalar variables.We show examples in which the technique is used to reason about arrays as well as string-keyed dictionaries. The approach was also experimentally evaluated.