Precise and efficient groundness analysis for logic programs.
We show how precise groundness information can be extracted from logic programs. The idea is to use abstract interpretation with Boolean functions as approximations to groundness dependencies between variables. This idea is not new, and different classes of Boolean functions have been used. We argue, however, that one class, the positive functions, is more suitable than others. Positive Boolean functions have a certain property which we (inspired by A. Langen) call condensation. This property allows for rapid computation of groundness information.
Introduction
Groundness analysis is arguably the most important dataflow analysis for logic programs. The
question: "At a given program point, is variable x always bound to a term that contains no vari-
ables?" is not only important for an optimizing compiler attempting to speed up unification, but
for practically every programming tool which applies some kind of dataflow analysis. The reason
is that most other analyses, such as independence analysis (whether instantiation of x indirectly
instantiates other variables) or occur-check analysis (whether unification can safely be performed
without the occur-check) employ groundness analysis to improve accuracy. For example, if x is
ground (a terminological abuse we consistently use for "bound to a ground term"), then x cannot
possibly share with other variables, and this is useful information for independence, occur-check,
and many other dataflow analyses.
Dataflow analysis of logic programs is different from the analysis of imperative or functional
programming languages. This is partly because the language is nondeterministic, but, more impor-
tantly, because dataflow in a sense is bidirectional, owing to the use of unification. The point is that
a variable in a logic programming language is very different from a variable in the other language
paradigms. It is sometimes referred to as a "logical variable" and characterized as "constrain-only"
since the execution of a logic program proceeds by steps that continually narrow the set of possible
values that a variable may take.
While this characteristic of logic program execution makes dataflow analyses harder in some
ways, it also opens up new views of some analysis problems. For example it suggests the possibility
of propagating conditional invariants of the form "From this point on, if variable x has (ever gets)
property p, then variable y has (will have) property r ." In this note we show how this applies to
groundness. The idea is to let the statement "program variable x is ground" be represented by the
propositional variable x . A groundness dependency such as "whenever y becomes ground, so does
may then be represented by a Boolean function, in this case the function denoted by y ! x . If
we use Boolean functions as approximations to runtime states, then abstract interpretation gives a
natural way of specifying a very precise groundness analysis (Sections 2 and 3).
This idea is not new, and different classes of Boolean functions have been used for the purpose.
The main purpose of this note is to show that exactly one of the classes, the positive functions,
has a very useful property which we shall refer to as "condensation" (Section 4). Owing to this
property, a relatively simple and efficient implementation is possible, yielding an extremely precise
analysis. The analysis is efficient partly because it is query-independent. We describe the analysis
in Section 5 and give a novel program transformation which makes it straightforward to extract
information about runtime call patterns.
Furthermore, the analysis can be performed in an incremental fashion without loss of accuracy
(Section 6). That is, dataflow information pertinent to a module may be computed independently of
the predicates imported by that module. This is because the class of positive functions is not only
condensing but also closed under existential quantification. Unfortunately quantifier elimination
is expensive in the presence of Boolean functions that are unknown, so the precision-preserving
extension of our analysis to modular programs may be of mainly theoretical interest.
Abstract interpretation of logic programs
Consider the idea of a logic program interpreter which answers queries by returning not only a set
of answer constraints, but also a thoroughly annotated version of the program: For each program
point it lists the constraints that are obtained there at some stage during evaluation of the given
query. Since control may return to a program point many times during evaluation, each annotation
is naturally a (possibly infinite) set of constraints.
Properly formalized, this idea leads to the notion of a collecting semantics, a semantics which
gives very precise dataflow information, but which is of course not finitely computable in general.
However, if we replace the possibly infinite sets of constraints by more crude "approximations" or
"descriptions" of sets of constraints, then we may obtain a dataflow analysis which terminates in
finite time. This is the idea behind abstract interpretation of logic programs.
Example 2.1 For the program
and query /q(a; x ), the collecting semantics associates
a
fl. A more crude approximation to this associates with a
sets that are
greater than or equal to those given by the collecting semantics. If we introduce the notation fug
for "the set of constraints that ground u" then associating fug with both a
fl is a correct
approximation. Though not very precise, it still tells us that every spawned query will have a ground
first argument.
This leads to the view that a dataflow analysis is an approximation to the collecting semantics.
P. and R. Cousot [6] have formalized that idea as follows. The standard domain Y (the powerset of
constraints in the example) and the description domain X (the powerset of variables in the example)
should be complete lattices with the monotonic giving the meaning of the descriptions
in X . Furthermore, fl X , the image of X under fl, should be a Moore family, that is, closed under
the greatest lower bound operation on Y . In Example 2.1 we have
grounds every
The ordering on the sets of variables is superset ordering in this case. This is because a larger set
of constraints will have fewer variables made ground by all constraints in the set. In general the
ordering on the lattice of descriptions is opposite to that normally used in denotational semantics:
a "higher" description applies to a larger set of constraints, that is, it has less information contents.
So "higher" means "less precise."
The notion of approximation is made exact as follows: x
We write this x / y . For syntactic objects, such as programs and primitive constraints, S / S 0 iff
Finally we extend / to function spaces as follows. Consider
We define f / g iff 8 x
A formal semantics can be given by laying down the appropriate semantic domains and specifying
certain operators on these domains. For groundness analysis there is only one important operation,
add , which takes a term equation and a set of constraints and forms the possible conjunctions:
An important feature of P. and R. Cousot's ``adjoined'' framework is that given an operation on
the standard domain, there is a least, that is, most precise, operation on the description domain
which approximates it. This is because descriptions form a Moore family. We shall refer to such
"most precise" operations as the induced operations. In general, the unique induced approximation
to
When referring to an induced groundness analysis we mean the analysis obtained by using the
induced version of add .
3 Groundness analysis using Boolean functions
As we have seen, a very natural description domain for groundness analysis are sets of variables
which are definitely ground at a particular program point. Such descriptions were introduced by
Mellish and used in early mode and groundness analyzers [11, 18]. We regard the set fx 1 ; :::; x n g as
representing the n-place Boolean function x 1 - x n to which we attach the meaning: at this
point all of the (program) variables x are bound to ground terms. We let Con be the set
of all such conjunctions of variables. Con is the simplest useful description domain for groundness
analysis, as anything less expressive cannot capture the type of statements that we require from
any groundness analysis.
However, Con does not lead to very precise groundness analysis because it ignores "aliasing"
and other dependencies between variables, witness the following example (from here on we only
label program points of interest).
Example 3.1 Consider the following program and query q(x ; y).
r(a)
An analysis based on Con will deduce that x will be ground at b
fl, but fail to deduce that y will
also be ground. The fact that x and y are aliases is not captured.
Aliasing information can be captured by more complex Boolean functions in which implication is
allowed. As an example, if the constraint during query evaluation, the
description x can be deduced. Informally the formula says that if x is (becomes)
ground then so is (does) both of y and z , and vice versa. Such Boolean formulas, called dependency
formulas, were introduced by Dart and used for groundness analysis in deductive databases [7, 8].
We denote the set of dependency formulas by Def , since they correspond to the Boolean functions
that can be written as definite propositional formulas. If the program in Example 3.1 is analyzed
using dependency formulas as descriptions, a
will have the description x
will have the description x - y , as desired.
Dependency formulas give rise to very precise groundness analyses. However, an even more
precise groundness analysis is possible with Pos , the set of positive Boolean functions. These
extend allowing disjunction. Pos was suggested for groundness analysis by Marriott and
S-ndergaard [14] (under the less suggestive name 'Prop') and further studied by Cortesi et al. [5].
Example 3.2 Consider the following program and query q(x ; y).
p(a; u)
An analysis based on cannot deduce that either x or y are ground at b
fl. The best description
it can produce is x $ y . However an analysis using Pos will find that a
fl has the description x - y ,
and so, by conjoining this information with x (from r) it finds that at b
both x and y are
ground.
In practice it is not common for programs to require the extra precision of Pos . Nonetheless we
feel that Pos is the better description domain for groundness analysis. This is because Pos has an
important property which allows it to be more efficiently implemented. This is somewhat surprising,
because one would expect extra precision to come at the cost of efficiency. The reason is that Pos
is closed under disjunction and so is "condensing," a property we discuss in Section 4. In the
remainder of this section we will formalize Pos and the other description domains.
We note that Pos is the largest class of Boolean functions which it makes sense to use as
descriptions in a groundness analysis. Since groundness is undecidable, a dataflow analysis operating
in finite time can only give approximate groundness information. The statements that it produces
will carry a modality, as in "x is inevitably ground." For this reason, only the positive Boolean
functions are useful. If we associate the meaning "x is inevitably ground" with the formula x , then
:x would mean "x may not always be ground" and this contains no information at all, that is,
exactly the information conveyed by the constant function true.
Definition. A Boolean function is a function F : Bool n ! Bool . We call the set of all n-ary
Boolean functions Bfun n and let it be ordered by logical consequence (j=). The function F is
positive iff F true. We denote the set of positive Boolean functions of n variables
by Pos n .
For simplicity we will assume that we have some fixed number n of variables and leave out subscripts
and the phrase "of n variables." We shall also use propositional formulas as representations of
Boolean functions without worrying about the distinction. Thus we may speak of a formula as if
it were a function and in any case denote it by F . As a reminder of the fact that a propositional
formula is only one of a class which all represent a given Boolean function, we put square brackets
around propositional formulas and think of the result as the class of equivalent formulas. By a slight
abuse of notation we sometimes apply logical connectives to these classes of equivalent formulas.
It is well known that Bfun is a Boolean lattice and in fact Pos forms a Boolean sublattice of
Bfun. In terms of propositional formulas, meet and join are given by conjunction and disjunction,
respectively.
Example 3.3 The Boolean functions [x are in Pos , but [:x ] is not.
It is convenient to include the (non-positive) Boolean function false as an approximation to the
empty set of constraints. So we will in fact be dealing with the complete lattice
ordered by logical consequence.
Let Sub denote the set of substitutions and let Eqn denote the set of constraints. In the Prolog
setting of this note, constraints are possibly existentially quantified term equations, but the ideas
generalize naturally to constraint logic languages. A substitution ' is a unifier of the constraint e
iff denote the set of unifiers of e. The idea with using Pos? is that a constraint
e is described by OE 2 Pos? exactly in case that, for every unifier ' of e, the truth assignment
corresponding to the variables ground by ' satisfies OE.
Definition. For a substitution ', let grounds ' be the truth assignment which maps a variable to
true if ' grounds the variable and to false otherwise. That is, grounds
defined by
grounds
where vars S is the set of variables in syntactic object S . The function
defined by
Thus fl maps OE 2 Pos? to the set of constraints e which have the property that, no matter how they
further become constrained to some e 0 , the Boolean function corresponding to e 0 will still satisfy OE.
Example 3.4 The Boolean function [x describes both of the constraints
not the constraint is not the best
description for b. For this constraint the best description is [x - y ] which in turn has
as a logical consequence. That is, [x is a less precise approximation than [x - y ].
As a further example, let approximated by OE
but not.
Proposition 3.1 [17] fl Pos? is a Moore family.
Let us define Con and
Let Def be the largest class of positive Boolean functions whose models are closed
under intersection and let Con be the monotonic functions in
Like are Moore families, so Con and are applicable as
domains for groundness analysis. It is well known that existential quantifiers can be eliminated
from Boolean functions, as 9 x What is perhaps less
obvious is the fact that Con, are all closed under existential quantification. This
simplifies their use in groundness analysis, since an important operation is the "projection" away
from variables that have become uninteresting, and the projection operation is exactly existential
quantification.
Condensation
Sometimes optimizations performed by a compiler are only applicable for certain types of queries.
For this reason, most dataflow analyses that have been suggested for logic programs are query
directed. That is, they compute an approximation to the collecting semantics for a particular query
description.
As we have seen, the collecting semantics gives information about program points. In particular
it gives information about calls to a predicate and the answers to a predicate. For instance, in
Example 3.2, a
collects information about the calls to r(x ; y) and b
collects information about
the answers to q(x ; y).
Information about the calls and answers may also be computed in a query-independent fashion.
In this case, the analysis is performed for all possible queries. This has the advantage that only
one analysis is performed, even when information about many different queries is needed, since
information about a particular query can be efficiently derived from the result of a query-independent
analysis.
Unfortunately the result from such a two-step process may well be less precise than that obtained
from separate query-directed analysis. This will be apparent from Example 4.1 below. However, one
point of this note is that there are cases in which no precision is lost by using a query-independent
analysis. This happens when a domain is "condensing." The name comes from the "condensing
procedures" introduced by Langen [12] and used by Jacobs and Langen [10] in their work on dataflow
analysis of logic programs.
We can think of a query-directed dataflow analysis as a function which takes a program, a query,
and possibly a statement about the initial state of variables in the query, yielding a statement about
the answers. Fixing the program P and the query Q , we may write the function as F \Phi
where \Phi is the domain of descriptions, or statements, available. We put the superscript \Phi as a
reminder of the fact that the dataflow analysis is the one induced by \Phi. A precise denotational
definition of F \Phi
for parametric \Phi can be found in [17].
Definition. The description domain \Phi is condensing iff
F \Phi
for all programs P , queries Q , and statements OE; OE 0 2 \Phi.
Note that in particular F \Phi
P;Q true). This means that an analysis with respect to
program P and query Q need not be repeated for several different OE. It only needs to be performed
in the most general case (true) where we make no assumptions about the instantiation of variables
whatsoever. If this yields OE 0 then the required answer is OE - OE 0 . This applies not just to the top-level
query, but to every call made during the execution of P .
Also note that the definition of condensing only considers the answers to a query. However, as
we shall see, condensation also allows us to compute information pertaining to arbitrary program
points.
Example 4.1 Consider the program P and query Q from Example 3.2. We have
F Con
F
F Pos
This illustrates the relative accuracy of the three domains. Furthermore,
F Con
F
so Con and Def are not condensing.
Our use of "condensing" is somewhat different from that of Jacobs and Langen. Our notion is
stronger, as we consider only the induced analysis F \Phi
P;Q . This is what makes it possible to consider
"condensing" a property of the domain \Phi. Jacobs and Langen allow for sub-optimal analyses,
the idea being that sometimes condensation can be achieved by introducing loss of accuracy in
the analysis. Even though the notions differ, the following result can be obtained by combining
Theorems 14, 65, 67, and 68 of Langen [12] since the operations Langen uses with Pos are in fact
the induced operations (this is not the case for other domains in Langen's treatment).
Theorem 4.1 Pos? is condensing.
We saw that Con? and are not condensing. In fact since closure under both - and ! are
necessary for condensation, we have:
Theorem 4.2 Pos? is the smallest extension of Con? which is condensing.
To summarize: As Pos? is condensing, groundness analysis using Pos can be modular. Once we
have a closed form for the result of calling predicate p, we need not worry about the context in
which p is called, or compute p's result for different environments.
5 Efficient groundness analysis
Debray [9] has shown that an analysis using Pos is in effect solving an EXPTIME-complete problem,
where complexity is measured in terms of program size. However, under the reasonable assumption
that the number of variables in any clause is bounded, an analysis using Pos is in PTIME. In
fact, a number of independent implementations of Pos indicate that accurate groundness analysis
is perfectly practical for "real-world" programs. A natural representation for Boolean functions,
used for example by Le Charlier and Van Hentenryck [13], is by means of ordered binary-decision
graphs [1]. Le Charlier and Van Hentenryck report good results from instantiating a generic "ab-
stract interpreter" with Pos .
But precise groundness analysis can be performed in an even more efficient way, as Pos is
condensing. While what we want is information about the calls that take place in a top-down
execution, it suffices to compute only "bottom-up" information which gives an approximation to
the answers of the program [16]. We first explain how to compute answer information.
Example 5.1 Let P be the program
As a first step we form the Clark completion [2] of
A straightforward translation yields the following recursive definitions of the Boolean functions
overlap and member :
Solving these (for member first, then for overlap), using Kleene iteration, we get
member 0 (u;
member 1 (u;
It is easy to verify that member 1 and overlap 1 make up a fixpoint and so are least solutions to the
system of recursive Boolean equations.
These results tell us for example that if member(u; y) is called with a groundness statement OE then
the result will be OE - [y ! u]. As far as overlap is concerned, the analysis cannot say anything
about groundness or groundness dependencies. This is adequate, since overlap does not in fact
introduce any groundness.
As a second example, let us compute the groundness information for the well-known append
program and the naive list reversal program. This is more interesting than the example above, as
it requires more iteration steps.
Example 5.2 The programs are
The corresponding Boolean functions are defined by
9
The equation for app is solved by the iteration
9
9
This is the least solution to the recursive definition of the Boolean function app. Using this we can
now solve for
which is the least solution to the recursive definition of rev .
Condensation also allows the efficient computation of (query-directed) information about calls occurring
at runtime. The idea is to use a program transformation which augments the program with
predicates whose answers are the calls occurring in the original program. Given a program point
a
fl in a clause
we define a new predicate q a
n ) which holds if and only if a call to q(x
spawns the call to p(y #
immediately after a
fl. As before, this gives rise to a recursive
definition of a Boolean function q a
which we can then compute once and for all. We illustrate this
with two examples.
Example 5.3 We repeat part of the program from Example 5.1 for convenience:
Assume we are interested in the calls to member at point a
fl in the context of a query to overlap.
As a first step we construct the new predicate
overlap a
overlap a
The two clauses come from the two original clauses, respectively. Continuing as before we get:
overlap a
Solving this equation, we get
overlap a
overlap a
This is the least fixpoint for the equation that defines overlap a
fl. It tells us for example, that at a
fl,
member will be called with a ground second argument if and only if overlap is called with a ground
second argument.
Example 5.4 Now assume we are interested in the calls to app at point a
fl in the program in
Example 5.2, in the context of a query to rev . The transformation step gives the recursive predicate:
rev a
rev a
The corresponding Boolean function is defined by
rev a
The equation for rev a
solved by the iteration
rev a
rev a
rev a
This tells us that if rev(x ; y) is called with x ground then calls to app at program point a
will have
the first and second arguments ground.
In short, our query-independent analysis gives information about calls and answers. Owing to
condensation, the result contains sufficient information that the result with respect to a specific
query can be derived efficiently and with no loss of accuracy. The positive Boolean functions
contain sufficient information about groundness dependencies to handle every possible call context
by simply conjoining functions. This speeds up computation and is simpler than more general
query-directed implementations of Pos .
The transformation given here generalizes the well-known magic-set transformation, which can
be used to compute information about the calls for a single query, see for example [19]. Codish
and Demoen [4] have independently investigated query-independent groundness analysis based on
Pos . While they do not consider precision, Codish and Demoen have implemented their analysis.
Their experimental results are most encouraging, especially as in the Codish/Demoen approach,
the computation of query-independent information about call patterns requires the computation of
a fixpoint, whereas in our approach, only a single conjunction is required for each program point.
6 Incremental groundness analysis
Groundness analysis using Pos may be incremental, that is, the dataflow information pertinent to a
module may be computed for the module, independently of the predicates it imports. We illustrate
the basic idea with two examples.
Example 6.1 Consider again the definition of overlap:
but now assume that the definition of member is not available. However, we can still analyze overlap
by solving the recursive equation
Kleene iteration gives:
This is the least solution to the equation for overlap.
Later, when the result for member arrives it can be plugged in, giving the result for overlap.
For example, if member(u; y) turns out to have the description [u - y ], that is, it always grounds
its arguments, then the description for overlap(x ; y) will be [y ]. Actually, we know from Section 5
that member(u; y) is approximated by the Boolean function [y ! u]. When this is substituted in
the formula for overlap, we obtain [true], as expected.
Example 6.2 Now consider the definition of the ancestor relationship which is defined in terms of
the parent relation.
We can analyze ancestor by solving the recursive equation
Kleene iteration gives:
ancestor
which is the least solution to the equation for ancestor . Later, the result for parent can be substi-
tuted, giving the result for ancestor . For example, if parent(x ; y) turns out to have the description
then the description for ancestor(x ; y) will be [x - y ].
There are three observations to make about the method illustrated in these examples.
1. It is generally applicable, even in the context of mutually recursive modules. Once the equations
are combined then, if they are mutually recursive, Kleene iteration can be used to solve
the system. In the case they are not mutually recursive, simple substitution suffices.
2. It will always terminate after a finite number of iterations with a finite approximation. This
is because the descriptions for the missing predicates are functions in Pos , and Pos is closed
under existential quantification. Thus, we can perform quantifier elimination to remove the
local variables, leaving only the constants true and false or non-quantified variables.
3. Performing the analysis incrementally does not change the result, that is, no accuracy is lost.
This is because Pos is condensing.
Unfortunately, although the analysis will always terminate, it is not clear that it can be implemented
efficiently, as for some practical programs analyzed by hand, the resulting equations are very large.
This blow-up is caused by applying quantifier elimination to the missing descriptions, and it is
difficult to see how it can be reduced.
Codish et al. [3] have given a general framework for incremental analysis based on an "unfold-
ing" semantics. The particular analysis sketched here differs from analyses in their framework in
two ways. First, because of the use of quantifier elimination, there is no need to introduce "star
abstractions" as our analysis will always terminate. Second, performing the analysis incrementally
never loses precision. This is because Pos is condensing, and because star abstraction is not used.
In the more general case of [3] no assumption of condensation can be made, so that performing an
analysis incrementally may lose precision.
7 Conclusion
Groundness analysis is an important component of most dataflow analyses for (constraint) logic
programs. In general, combination of dataflow analyses is not easy, but for most composite analyses
it turns out that the groundness component may be computed separately, first, and the groundness
results may then be used by other analyses, without this staging having negative effects on accuracy.
For this reason, it is important that groundness analysis be accurate while still efficient.
Pos gives rise to one of the most precise groundness analyses that we know of. In particular it
achieves more accuracy than more complex analyses based on "reexecution" or "propagation" [15].
By utilizing condensation it is possible to implement groundness analysis based on Pos efficiently.
This is empirically supported by the recent implementation of Codish and Demoen [4]. A further
advantage of Pos is that the analysis may be incremental, that is, the dataflow information pertinent
to a module may be computed for the module, independently of the predicates it imports and with
no loss of accuracy.

Acknowledgements

We thank Mike Codish and an anonymous referee for useful suggestions that have improved this
paper.



--R

Symbolic Boolean manipulation with ordered binary-decision diagrams
Negation as failure.
Compositional analysis of modular logic programs.
"Prop"-ositional logic programs and a magic wand
abstract domain for groundness analysis.
Systematic design of program analysis frameworks.
Dependency Analysis and Query Interfaces for Deductive Databases.
On derived dependencies and connected databases.
On the complexity of dataflow analysis of logic programs.
Static analysis of logic programs for independent and paral- lelism
A semantics-based framework for the abstract interpretation of Prolog
Advanced Techniques for Approximating Variables in Logic Programs.
Groundness analysis for Prolog: Implementation and evaluation of the domain Prop.
Notes for a tutorial on abstract interpretation of logic programs.
On propagation-based analysis of logic programs

Denotational abstract interpretation of logic programs.
Some global optimizations for a Prolog compiler.
Abstract interpretation: A kind of magic.
--TR
On derived dependencies and connected databases
Symbolic Boolean manipulation with ordered binary-decision diagrams
Static analysis of logic programs for independent and parallelism
Groundness analysis for Prolog
Compositional analysis of modular logic programs
Denotational abstract interpretation of logic programs
Analysing logic programs using MYAMPERSANDldquo;propMYAMPERSANDrdquo;-ositional logic programs and a magic wand
Abstract interpretation
Systematic design of program analysis frameworks
On the Complexity of Dataflow Analysis of Logic Programs
Advanced techniques for approximating variable aliasing in logic programs

--CTR
Vitaly Lagoon , Peter J. Stuckey, Precise pair-sharing analysis of logic programs, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.99-108, October 06-08, 2002, Pittsburgh, PA, USA
Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Making abstract domains condensing, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.33-60, January 2005
Michael Codish , Harald Sndergaard , Peter J. Stuckey, Sharing and groundness dependencies in logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.5, p.948-976, Sept. 1999
Francesca Scozzari, Logical optimality of groundness analysis, Theoretical Computer Science, v.277 n.1-2, p.149-184, April 28, 2002
Andy King , Lunjin Lu, A backward analysis for constraint logic programs, Theory and Practice of Logic Programming, v.2 n.4-5, p.517-547, July 2002
Jacob M. Howe , Andy King, Efficient groundness analysis in Prolog, Theory and Practice of Logic Programming, v.3 n.1, p.95-124, January
Saumya K. Debray, On the complexity of dataflow analysis of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.2, p.331-365, March 1995
Agostino Complementation in abstract interpretation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.7-47, Jan. 1997
Giorgio Levi , Fausto Spoto, Pair-independence and freeness analysis through linear refinement, Information and Computation, v.182
Kim Marriott , Harald Sndergaard , Neil D. Jones, Denotational abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.607-648, May 1994
Maurice Bruynooghe , Michael Codish , John P. Gallagher , Samir Genaim , Wim Vanhoof, Termination analysis of logic programs through combination of type-based norms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.2, p.10-es, April 2007
Marc Denecker , Maurice Bruynooghe , Victor Marek, Logic programming revisited: logic programs as inductive definitions, ACM Transactions on Computational Logic (TOCL), v.2 n.4, p.623-654, Oct. 2001
Roberto Giacobazzi , Francesca Scozzari, A logical model for relational abstract domains, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.5, p.1067-1109, Sept. 1998
Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Making abstract interpretations complete, Journal of the ACM (JACM), v.47 n.2, p.361-416, March 2000
Roberto Bagnara , Roberta Gori , Patricia M. Hill , Enea Zaffanella, Finite-tree analysis for constraint logic-based languages, Information and Computation, v.193 n.2, p.84-116, 15 September 2004
propositional logic;condensation;abstract interpretation;groundness analysis