Tech Report CS-90-25
A Generic Abstract Interpretation Algorithm and its Complexity Analysis (extended abstract)
Baudouin Le Charlier, Kaninda Musumbu and Pascal Van Hentenryck
A generic abstract interpretation algorithm for Prolog programs is presented and its complexity analyzed. The algorithm is parametrized on the abstract domain and can be instantiated by choosing an abstraction of substitutions and an implementation of a number of abstract operations whose specifications are given as consistent abstractions of some concrete operations. The algorithm, which is representation-independent, has been developed by successive refinements from the abstract semantics and includes optimizations such as the detection of definitive results, the early recognition of termination, and the detection of dynamic dependencies. The worst-case complexity of the algorithm is analyzed for various classes of programs and behavioral assumptions.
(complete text in pdf)