Symbolic Implementation of the Best Transformer
AUTHORS Thomas Reps, Mooly Sagiv, and Greta Yorsh
We show 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. This talk does not assume prior knowledge in abstract interpretation or shape analysis.