Symbolic Implementation of the Best Transformer

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 )