Record Details


Field	Value

Title	Automatically refining abstract interpretations

Names	GULAVANI, BS CHAKRABORTY, S NORI, AV RAJAMANI, SK
Date Issued	2008 (iso8601)
Abstract	interpretation techniques prove properties of programs by computing 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 refinement, and (3) a new refinement algorithm, which refines abstract interpretations 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 that are beyond current abstraction-refinement tools, such as SLAM [4], BLAST [15], ARMC [19], and our earlier tool [12].
Genre	Proceedings Paper
Topic	Refinement
Identifier	TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS,4963,443-458

ICAR Research Data Repository for Knowledge Management