Refining Abstract Interpretations

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

Abstract

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.

Details

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