Skip to main content

Practical Model-Based Static Analysis for Definite Logic Programs

John Gallagher, Dmitri Boulanger, Huseyin Saglam, Practical Model-Based Static Analysis for Definite Logic Programs. CSTR-95-011, Department of Computer Science, University of Bristol. June 1995. PDF, 296 Kbytes.


The declarative semantics of definite logic programs is the basis of an elegant and practical framework for their static analysis. We define a core semantics parameterised by a pre-interpretation of the language underlying the program. The concrete semantics is given by an extended Herbrand interpretation, capturing the correct answers of a program. The semantics is computed as the least fixed point of an immediate consequences operator. An abstract semantics is specified simply by giving, for each constant and function in the program, a denotation in an abstract domain of interpretation. No abstract operations such as abstract unification need to be defined. The directness and simplicity of this approach is then illustrated by specifying and implementing a number of abstract interpretations. These include various mode analyses, analyses on the structure of lists and the length of lists, and simple and polymorphic types. The implementations used for the experiments are based on abstract compilation and existing bottom-up analysis tools. Even without any domain-specific optimisations, the results indicate that the approach is practical for many useful domains.

Bibtex entry.

Publication Admin