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

Publisher  Elsevier
Copyright © 2007 Elsevier B.V. All rights reserved.

Details