Automated Verification of Prolog Programs

Although Prolog is (still) the most widely used logic language, it suffers from a number of drawbacks which prevent it from being truely declarative. The nondeclarative features such as the depth-first search rule are nevertheless necessary to make Prolog reasonably efficient. Several authors have proposed methodologies to reconcile declarative programming with the algorithmic features of Prolog. The idea is to analyse the logic program with respect to a set of properties such as modes, types, sharing, termination, and the like in order to ensure that the operational behaviour of the Prolog program complies with its logic meaning. Such analyses are tedious to perform by hand and can be automated to some extent. This paper presents a state-of-the-art analyser which allows one to integrate many individual analyses previously proposed in the literature as well as new ones. Conceptually, the analyser is based on the notion of abstract sequence which makes it possible to collect all kinds of desirable information, including relations between the input and output sizes of terms, multiplicity, and termination