Thomas Reps, Mooly Sagiv, and Greta Yorsh
In Proc. Verification, Model Checking, and Abstract Interpretation, 2004 (VMCAI 2004)
This paper shows how to achieve, under certain conditions, abstract-interpretation algorithms that enjoy the best possible precision for a given abstraction. The key idea is a simple process of successive approximation that makes repeated calls to a theorem prover, and obtains the best abstract value for a set of concrete stores that are represented symbolically, using a logical formula.
(Click here to access the paper: PostScript; PDF; Slides )