Counterexample Driven Refinement for Abstract Interpretation - Gulavani, Bhargav; Rajamani, Sriram (Proceedings of 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2006)
Abstract interpretation techniques prove properties of programs by computing abstract ﬁxpoints. All such analyses suﬀer from the possibility of false errors. We present a new counterexample driven reﬁnement technique to reduce false errors in abstract interpretations. Our technique keeps track of the precision losses during forward ﬁxpoint computation, and does a precise backward propagation from the error to either conﬁrm the error as a true error, or identify a reﬁnement so as to avoid the false error. Our technique is quite simple, and is independent of the speciﬁc abstract domain used. An implementation of our technique for aﬃne transition systems is able to prove invariants generated by the StInG tool [19] without doing any specialized analysis for linear relations. Thus, we hope that the technique can work for other abstract domains as well. We sketch how our technique can be used to perform shape analysis by simply deﬁning an appropriate widening operator over shape graphs.