|Publication Type||Conference Paper|
|Year of Publication||1999|
|Authors||Hill PM, Spoto F|
|Editor||Cortesi A, Filé G|
|Conference Name||Static Analysis: Proceedings of the 6th International Symposium|
|Keywords||abstract interpretation, freeness analysis, linear refinement, logic programming, mode analysis, software verification, static analysis|
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 for the first time uses linear refinement to construct a new domain instead of just reconstructing an existing one. This domain is designed for definite freeness analysis and consists of sets of dependencies between sets of variables. We provide explicit definitions 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.