Non Pair-Sharing and Freeness Analysis through Linear Refinement

Linear refinement is a technique for systematically constructing abstract domains for program analysis directly from a basic domain representing just the property of interest. This paper uses linear refinement to construct a domain for non pair-sharing and freeness analysis. The resulting domain is strictly more precise than the domain for sharing and freeness analysis defined by Jacobs and Langen. Moreover, it can be used for abstract compilation, while Jacobs and Langenʹs domain can only be used for abstract interpretation. We provide a representation of the domain, together with algorithms for the abstract operations.