This paper demonstrates shape analyses that can achieve a state space
reduction exponential in the number of threads, while retaining
sufficient precision to verify sophisticated properties such as
linearizability.  The key idea is to abstract the global heap by
decomposing it into subheaps, losing correlations between them, in a
state-sensitive fashion.  We consider sequential and concurrent
programs, with both coarse- and fine-grained control.  Abstraction by
decomposition can be used to approximate and achieve thread-modular
abstractions, but need not be so imprecise.

These new shape analysis algorithms are instances of an analysis
framework based on heap decomposition, which we present here.  The
chief technical challenge was developing a flexibly-specified family
of sound, precise, and efficiently computable abstract transformers.
We have implemented this abstraction framework in a system that allows
rapid prototyping of complex static analyses by specifying different
decomposition schemes.  Our initial results confirm the value of heap
decomposition in scaling concurrent shape analyses.