Freeness Analysis through Linear Refinement.
Patricia Munday Hill, Fausto Spoto · 1999
Linear renement is a technique for systematically constructing abstract domains for program analysis directly from a basic domain representing just the property of interest. This paper for the rst time uses linear renement to construct a new domain instead of just reconstructing an existing one. This domain is designed for denite freeness analysis and consists of sets of dependencies between sets of variables. We provide explicit denitions of the operations for this domain which we show to be safe with respect to the concrete operations. We illustrate how the domain may be used in a practical analysis by means of a small example. Keywords: Abstract interpretation, abstract domain, linear renement, static analysis, freeness analysis, logic programming. 1 Introduction Linear renement [13] is a technique for systematically constructing abstract domains for program analysis. Given a basic abstract domain representing just the property of interest together with an appropriate concre...