We present a methodology for automatically combining abstract interpreters over given lattices to construct an abstract interpreter for the combination of those lattices. This lends modularity to the process of design and implementation of abstract interpreters.
We define the notion of logical product of lattices. This kind of combination is more precise than the reduced product combination. We give algorithms to obtain the join operator and the existential quantification operator for the combined lattice from the corresponding operators of the individual lattices. We also give a bound on the number of steps required to reach a fixed point across loops during analysis over the combined lattice in terms of the corresponding bounds for the individual lattices.
We also present an interesting application of logical product wherein some lattices can be reduced to combination of other (unrelated) lattices with known abstract interpreters.
pdf.
@inproceedings{GulwaniTiwari06:PLDI,
author = "S. Gulwani and A. Tiwari",
title = "Combining abstract interpreters",
booktitle = {{ACM SIGPLAN} Conf. on Programming Language Design and Implementation, PLDI 2006},
year = 2006,
editor = "T. Ball",
pages = "??--??",
}