Refining Abstract Interpretations

Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, and Sriram K. Rajamani


Abstract interpretation techniques prove properties of programs by computing abstract fixpoints. All such analyses suffer from the possibility of false errors. We present a dag based abstraction refinement technique to automatically refine such abstract interpretations and reduce false errors. This technique refines precision loss due to widen operator by a new interpolated widen operator and refines precision loss due to join operator by disjunctions. We prove the soundness and progress properties of this abstraction refinement procedure.


Publication typeInproceedings
Published inInformation Processing Letters
> Publications > Refining Abstract Interpretations