Refining abstract interpretations

cally Refining Abstract Interpretations Bhargav S. Gulavani1 , Supratik Chakraborty1 , Aditya V. Nori2 , and Sriram K. Rajamani2 1 IIT Bombay 2 Microsoft Research India Abstract. Abstract interpretation techniques prove properties of procomputing abstract fixpoints. All such analyses suffer from the possibility of false errors. We present three techniques to automatically refine such abstract interpretations to reduce false errors: (1) a new operator called interpolated widen, which automatically recovers precision lost due to widen, (2) a new way to handle disjunctions that arise due to nt, and (3) a new refinement algorithm, which refines abstract tations that use the join operator to merge abstract states at join points. We have implemented our techniques in a tool Dagger. Our experimental results show our techniques are effective and that their combination is even more effective than any one of them in isolation. We also show that Dagger is able to prove properties of C programs be...

• Type: Journal
• Year: 2010
• Where: IPL
• Authors: Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, Sriram K. Rajamani
• Keywords: Abstract Interpretations, Abstract Interpretations Bhargav, False Errors, Image Processing, IPL 2010