In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently, the new domain ShLin^omega has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract operator for single-binding unification. The authors claim that the repeated application of this operator is also optimal for multibinding unification. This is the proof of such a claim.
Optimal multibinding unification for sharing and linearity analysis
AMATO, Gianluca;SCOZZARI, Francesca
2014-01-01
Abstract
In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently, the new domain ShLin^omega has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract operator for single-binding unification. The authors claim that the repeated application of this operator is also optimal for multibinding unification. This is the proof of such a claim.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
