Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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.