Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Lightweight Specialized 3-Valued Logic Shape Analyzer

Gilad Arnold

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2006-59
May 16, 2006

http://www.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},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2006},
    Month = {May},
    URL = {http://www.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://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-59.html
%F Arnold:EECS-2006-59