Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-23T11:08:07.392Z Has data issue: false hasContentIssue false
  • English
  • Français

A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages

Published online by Cambridge University Press:  16 April 2004

PATRICIA M. HILL ,
ENEA ZAFFANELLA  and
ROBERTO BAGNARA
PATRICIA M. HILL
Affiliation:
School of Computing, University of Leeds, Leeds, UK (e-mail: [email protected])
ENEA ZAFFANELLA
Affiliation:
Department of Mathematics, University of Parma, Parma, Italy (e-mail: [email protected])
ROBERTO BAGNARA
Affiliation:
Department of Mathematics, University of Parma, Parma, Italy (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

It is well known that freeness and linearity information positively interact with aliasing information, allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper, we present a novel combination of set-sharing with freeness and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in Bagnara et al. (2000) and Zaffanella et al. (2002) also applies to this abstract domain combination: this allows for the implementation of an abstract unification operator running in polynomial time and achieving the same precision on all the considered observable properties.

Keywords

abstract interpretationlogic programmingabstract unificationrational treesset-sharingfreenesslinearity
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 4 , Issue 3 , May 2004 , pp. 289 - 323
Copyright
© 2004 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

This work has been funded by MURST projects “Automatic Program Certification by Abstract Interpretation”, “Abstract Interpretation, type systems and control-flow analysis”, and “Automatic Aggregate- and Number-Reasoning for Computing: from Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps”; by the Integrated Action Italy-Spain “Advanced Development Environments for Logic Programs”; by the University of Parma's FIL scientific research project (ex 60%) “Pure and applied mathematics”; and by the UK's Engineering and Physical Sciences Research Council (EPSRC) under grant M05645.