In this paper, we show how separation (decomposing a
verification problem into a collection of verification
subproblems) can be used to improve the efficiency and precision
of verification of safety properties. We present a simple language
for specifying separation strategies for decomposing a
single verification problem into a set of subproblems. (The
strategy specification is distinct from the safety property
specification and is specified separately.) We present a general
framework of heterogeneous abstractions that allows
different parts of the heap to be abstracted using different
degrees of precision at different points during the analysis. We
show how the goals of separation (i.e., more efficient
verification) can be realized by first using a separation strategy
to transform (instrument) a verification problem instance
(consisting of a safety property specification and an input
program), and by then utilizing heterogeneous abstraction during
the verification of the transformed verification problem.