This is Enea.


Personal Info





Boolean Functions for Finite-Tree Dependencies (LPAR'01)

[Page last updated on "January 13, 2005, 15:31:42".]

Roberto Bagnara, Enea Zaffanella, Roberta Gori and Patricia M. Hill


Several logic-based languages, such as Prolog II and its successors, SICStus Prolog and Oz, offer a computation domain including rational trees that allow for increased expressivity and faster unification. Unfortunately, the use of infinite rational trees has problems. For instance, many of the built-in and library predicates are ill-defined for such trees and need to be supplemented by run-time checks whose cost may be significant. In a recent paper [1], we have proposed a data-flow analysis called finite-tree analysis aimed at identifying those program variables (the finite variables) that are not currently bound to infinite terms. Here we present a domain of Boolean functions, called finite-tree dependencies that precisely captures how the finiteness of some variables influences the finiteness of other variables. We also summarize our experimental results showing how finite-tree analysis, enhanced with finite-tree dependencies is a practical means of obtaining precise finiteness information.


R. Bagnara, R. Gori, P. M. Hill and E. Zaffanella.

Finite-Tree Analysis for Constraint Logic-Based Languages.
In P. Cousot, editor, Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, pages 165--184, Paris, France, 2001. Springer-Verlag, Berlin.

Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, and BibTeX entry.
© Enea Zaffanella

| Home | Personal Info | Research | Papers | Teaching | About