Record Details

Counterexample driven refinement for abstract interpretation

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Counterexample driven refinement for abstract interpretation
 
Creator GULAVANI, BS
RAJAMANI, SK
 
Description Abstr. interpretation techniques prove properties of programs by computing abstract fixpoints. All such analyses stiffer from the possibility of false errors. We present a new counterexample driven refinement technique to reduce false errors in abstract interpretations. Our technique keeps track of the precision losses during forward fixpoint computation, and does a precise backward propagation from the error to either confirm the error as a true error, or identify a refinement so as to avoid the false error. Our technique is quite simple, and is independent of the specific abstract domain used. An implementation of our technique for affine 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 defining an appropriate widening operator over shape graphs.
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-23T19:34:57Z
2011-12-15T09:10:44Z
2011-10-23T19:34:57Z
2011-12-15T09:10:44Z
2006
 
Type Article; Proceedings Paper
 
Identifier TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS,3920,474-488
3-540-33056-9
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15217
http://hdl.handle.net/100/1632
 
Source 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Vienna, AUSTRIA,MAR 25-APR 02, 2006
 
Language English