Shape analysis concerns the problem of determining ``shape
invariants'' for programs that perform destructive updating on
dynamically allocated storage.
TVLA (Three-Valued Logic Analysis) is a system for shape
analysis that can be used in different ways to create different
shape analysis implementations that provide varying degrees of
efficiency and precision.
A key property of TVLA is that the stores that can possibly arise
during execution are represented (conservatively) using sets of
3-valued logical structures.
While the TVLA system is general, this generality comes at a very
high price:
``Often the analysis of small programs is very expensive in terms of time and space.''
Indeed, the algorithms used in TVLA have very high complexity.
The overall complexity could be doubly exponential in the program size.
This thesis is aimed at improving the performance of static
analyses in the TVLA system, with the aid of new algorithms and
data structures. In the first part, new data structures, which
represent 3-valued first-order structures are shown to largely
reduce the space consumption. One of these data structures is
based on OBDDs (ordered binary decision diagrams) which are
widely used for finite state model checking. In the second part,
a reduction in the overall analysis cost is achieved by exploring
new abstractions that produce more compact sets of structures.