Chaotic fixpoint iteration guided by dynamic dependency

Abstract

An algorithm for abstract interpretation of logic programs is defined and analyzed. The algorithm is proved to be correct with respect to an abstract semantics for (a variant of) Prolog. This abstract semantics associates a given prograin with a function that maps each call pattern for a predicate to a distinct success pattern. The proposed algorithm employs a variant of chaotic iteration, and is based on what may be termed a dynamic dependency relation. A low worst-case complexity is achieved: the number of passes of dataflow analysis over each program clause is proved to be independent of the size of the rest of the program.