Tech Report CS-94-16

An Abstract Interpretation Framework for (almost) Full Prolog

B. Le Charlier, S. Rossi and P. Van Hentenryck

April 1994


A novel abstract interpretation framework is introduced that captures Prolog depth-first strategy and the cut operation. The framework is based on a new conceptual idea, the notion of substitution sequences, and the traditional fixpoint approach to abstract interpretation. It broadens the class of analyses that are amenable in practice to abstract interpretation and refines the precision of existing analyses. Its practicability is demonstrated in a companion paper. This paper focuses on theoretical foundations.

(complete text in pdf or gzipped postscript)