An abstract domain combinator for separately conjoining memory abstractions ⋆

Abstract. The breadth and depth of heap properties that can be inferred by the union of today’s shape analyses is quite astounding. Yet, achieving scalability while supporting a wide range of complex data structures in a generic way re-mains a long-standing challenge. In this paper, we propose a way to side-step this issue by defining a generic abstract domain combinator for combining mem-ory abstractions on disjoint regions. In essence, our abstract domain construction is to the separating conjunction in separation logic as the reduced product con-struction is to classical, non-separating conjunction. This approach eases the de-sign of the analysis as memory abstract domains can be re-used by applying our separating conjunction domain combinator. And more importantly, this combina-tor enables an analysis designer to easily create a combined domain that applies computationally-expensive abstract domains only where it is required.