Record Details

Automatically refining abstract interpretations

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Automatically refining abstract interpretations
 
Creator GULAVANI, BS
CHAKRABORTY, S
NORI, AV
RAJAMANI, SK
 
Subject refinement
interpolation
systems
 
Description 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].
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-23T23:26:05Z
2011-12-15T09:11:18Z
2011-10-23T23:26:05Z
2011-12-15T09:11:18Z
2008
 
Type Proceedings Paper
 
Identifier TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS,4963,443-458
978-3-540-78799-0
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15266
http://hdl.handle.net/100/1986
 
Source 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Budapest, HUNGARY,MAR 29-APR 06, 2008
 
Language English