Combining abstract interpreters

Sumit Gulwani and Ashish Tiwari

To be presented at PLDI 2006, Ottawa, Canada, June 10-16, 2006.


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.




BibTeX Entry

	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 = "??--??",

Return to the Ashish's home page
Return to the Computer Science Laboratory home page