Gilad Arnold

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2006-59

May 16, 2006

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-59.pdf

We describe the design and implementation of a specialized shape analysis tool based on 3-valued logic. Our analyzer can reason about programs manipulating recursive data structures, such as singly- and doubly-linked lists, yielding precise results that are comparable to those of the well-known reference implementation, in only a fraction of the time. In particular, (a) we apply a new and effective technique for performing structure-based abstraction refinement, and (b) introduce a new definition for ordering of abstract heap descriptors which leads to a significant deflation in the sets of abstract states explored by the analysis. Although currently restricted by design in its applicability for different flavors of analyses, we argue that---thanks to a modular and extendable architecture---generalizing the capabilities of our tool can be achieved by means of further mostly straightforward (yet non-trivial) software engineering effort.

---

BibTeX citation:

@techreport{Arnold:EECS-2006-59,
    Author= {Arnold, Gilad},
    Title= {Lightweight Specialized 3-Valued Logic Shape Analyzer},
    Year= {2006},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-59.html},
    Number= {UCB/EECS-2006-59},
    Abstract= {We describe the design and implementation of a specialized shape analysis tool based on 3-valued logic. Our analyzer can reason about programs manipulating recursive data structures, such as singly- and doubly-linked lists, yielding precise results that are comparable to those of the well-known reference implementation, in only a fraction of the time. In particular, (a) we apply a new and effective technique for performing structure-based abstraction refinement, and (b) introduce a new definition for ordering of abstract heap descriptors which leads to a significant deflation in the sets of abstract states explored by the analysis. Although currently restricted by design in its applicability for different flavors of analyses, we argue that---thanks to a modular and extendable architecture---generalizing the capabilities of our tool can be achieved by means of further mostly straightforward (yet non-trivial) software engineering effort.},
}

EndNote citation:

%0 Report
%A Arnold, Gilad 
%T Lightweight Specialized 3-Valued Logic Shape Analyzer
%I EECS Department, University of California, Berkeley
%D 2006
%8 May 16
%@ UCB/EECS-2006-59
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-59.html
%F Arnold:EECS-2006-59