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.
In Information Processing Letters
Copyright © 2007 Elsevier B.V. All rights reserved.