Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the safe omission of the occurs-check) and increased expressivity (cyclic terms can provide very efficient representations of grammars and other useful objects). 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. Moreover, some widely-used program analysis and manipulation techniques are correct only for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of the program variables (the *finite variables*) that, at the program points of interest, will always be bound to finite terms. For these reasons, we propose here a new data-flow analysis, based on abstract interpretation, that captures such information. We present a parametric domain where a simple component for recording finite variables is coupled, in the style of the *open product* construction of Cortesi et al., with a generic domain (the parameter of the construction) providing sharing information. The sharing domain is abstractly specified so as to guarantee the correctness of the combined domain and the generality of the approach. This finite-tree analysis domain is further enhanced by coupling it with 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.

The availability of good foreign language interfaces is fundamental for the interoperability of different programming languages. While this observation is true for any language, it is especially important for non-mainstream languages such as Prolog, since they are likely to be discarded when shortcomings of the interfaces suggest the adoption of just one implementation language. In this paper we review some existing Prolog foreign language interfaces, trying to highlight both the important characteristics they share and the features that distinguish them from one another. We argue that even a basic, but *standard* Prolog foreign language interface could significantly contribute to increasing the adoption of Prolog for those subsystems where it is {\textquoteleft}{\textquoteleft}the right language{\textquoteright}{\textquoteright}. Finally we suggest which steps could be taken in this direction.

Escape analysis of object-oriented languages allows us to stack allocate dynamically created objects and to reduce the overhead of synchronisation in Java-like languages. We formalise the *escape property* *E*, computed by an escape analysis, as an abstract interpretation of concrete states. We define the optimal abstract operations induced by *E* for a framework of analysis known as *watchpoint semantics*. The implementation of *E* inside that framework is a formally correct abstract semantics (analyser) for escape analysis. We claim that *E* is the basis for more refined and precise domains for escape 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.

}, keywords = {abstract interpretation, freeness analysis, linear refinement, logic programming, mode analysis, software verification, static analysis}, isbn = {3-540-66459-9}, doi = {10.1007/3-540-48294-6_6}, author = {Patricia M. Hill and Fausto Spoto}, editor = {Agostino Cortesi and Gilberto Fil{\'e}} }