A Toolkit for Static Analysis of Constraint Logic ProgramsHuseyin Saglam, A Toolkit for Static Analysis of Constraint Logic Programs. PhD thesis. Department of Computer Science, University of Bristol. December 1997. PDF, 784 Kbytes.
Generic systems for the analysis of logic programs have been proposed over the last decade or so. Considerable progress has been made in terms of frameworks, algorithms, abstract domains and implementations. A number of generic top-down procedural frameworks are widely available. However, implementation efforts for bottom-up declarative frameworks are in a preliminary stage. In this thesis we design and implement a program analysis framework for (constraint) logic programs. Our aim is to build a general purpose, versatile toolkit which is simple, practical and flexible, and provides reasonably precise approximations, as well as allowing complex analyses to be constructed for proving program properties. This is done by providing a set of general approximation techniques parameterised by a property of interest, which is defined using pre-interpretations. Abstract compilation is used to incorporate properties into the program to be analysed. Then a bottom-up fixpoint computation of an immediate consequences operator is performed. Goal dependent analyses are realised through a set of query-answer transformation options. Our framework is based on declarative semantics, in particular on the standard logical notions of interpretation, model and logical consequence, and avoids the classical complex procedural ingredients used in other frameworks. Constraint logic programming is used as a meta-languge to express properties of terms. A pre-interpretation is a CLP program with arbitrary complexity. We present the framework, introduce the components, options and combinations of the components, provide a guide for using the toolkit, and demonstrate a numb er of applications using the framework.