Making abstract domains condensing

By: R. Giacobazzi, F. Ranzato, and F. Scozzari

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie 15, Ca' Vignal 2, 37134 Verona (Italy)
roberto.giacobazzi@univr.it

Abstract:

In this paper we show that reversible analysis of logic languages by abstract interpretation can be performed without loss of precision by systematically refining abstract domains. The idea is to include semantic structures into abstract domains in such a way that the refined abstract domain becomes rich enough to allow approximate bottom-up and top-down semantics to agree. These domains are known as condensing abstract domains. Substantially, an abstract domain is condensing if goal-driven and goal-independent analyses agree, namely no loss of precision is introduced by approximating queries in a goal-independent analysis. We prove that condensation is an abstract domain property and that the problem of making an abstract domain condensing boils down to the problem of making the corresponding abstraction complete with respect to unification. In the case of abstract domains for logic program analysis approximating computed answer substitutions, condensing domains are provided with a clean logical interpretation as fragments of propositional linear-logic. We apply our method to the systematic design of condensing domains for freeness and independence analysis.

Available: soon!!