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.
Title
Lightweight Specialized 3-Valued Logic Shape Analyzer
Published
2006-05-16
Full Collection Name
Electrical Engineering & Computer Sciences Technical Reports
Other Identifiers
EECS-2006-59
Type
Text
Extent
29 p
Archive
The Engineering Library
Usage Statement
Researchers may make free and open use of the UC Berkeley Library’s digitized public domain materials. However, some materials in our online collections may be protected by U.S. copyright law (Title 17, U.S.C.). Use or reproduction of materials protected by copyright beyond that allowed by fair use (Title 17, U.S.C. § 107) requires permission from the copyright owners. The use or reproduction of some materials may also be restricted by terms of University of California gift or purchase agreements, privacy and publicity rights, or trademark law. Responsibility for determining rights status and permissibility of any use or reproduction rests exclusively with the researcher. To learn more or make inquiries, please see our permissions policies (https://www.lib.berkeley.edu/about/permissions-policies).
