Modern programs rely significantly on the use of dynamically-
allocated linked data structures.  Shape analysis algorithms
statically analyze a program to determine information about these
data structures, e.g, "does variable x point to an acyclic list?"
and "is it possible to reach an object via pointer traversals
from two different variables?" These algorithms are conservative
(sound), that is, the discovered information is true for every
program input, and thus can be applied for various uses, such as
program verification, optimization, parallelization, etc.

Disjunctive shape analyses operate by abstracting the concrete
memory stores into (bounded) shape graphs. At control flow join
points of the program, the shape graphs are merged by using
disjunction (set union), which often leads to an exponential
explosion in the number of shape graphs. In concurrent programs
this problem is even more acute, due to the interleaving of
different threads.

We present new "partially disjunctive" shape analyses aimed at
taming the size of the state space by abstracting disjunctions,
as well as soundly approximating program statements. We
implemented and applied these analyses to prove properties of
sequential programs and fine-grained concurrent programs. We were
able to prove a variety of challenging properties, including
cleanness properties, shape invariants, and linearizability of
concurrent data structure implementations. The new shape analyses
scale better than the disjunctive shape analyses, usually running
faster by orders of magnitude, and still able to prove the
desired properties.