Polyhedral Domains for Abstract Interpretation in Logic Programming

The motivations for program analyses are many. The impetus for the static analysis of programs initially ranged from the need for more efficient code to program transforms for parallel systems, but with the passage of time now also encompasses: providing the programmer with debugging information, program verification and program testing. Abstract interpretation is a methodology for static analysis that was formalised at the beginning of the last decade and is employed in both declarative and imperative programming paradigms. Abstract interpretation is a rigorous approximation technique that allows an analysis to focus on a particular property and infer useful information about the run time behaviour of the program being analysed. In order to implement an abstract interpretation it is necessary to chose an abstract domain that expresses the property of interest with sufficient precision to be useful. The focus of this thesis is on the use of two polyhedral domains as a means of capturing these properties of interest in logic programs. This thesis demonstrates how polyhedra can be employed to capture analyses that relate to dependency information with respect to some measure of size. Polyhedral analyses require a technique known as widening to ensure analysis convergence. Computational issues associated with widening prompted an investigation into the way linear spaces interact and how it is possible for a polyhedron to have different representations as a set of implicitly conjoined linear inequalities. Some useful computational insights are the outcome of this investigation. The observation that certain linear inequalities might represent dependency information prompted a novel approach to capturing dependency analysis with the subclass of polyhedra that can be represented by those linear inequalities. This could be advantageous for analyses in environments with constraint support as no set-up costs for the analysis would be incurred as the existing environment would be capable of supporting the abstract domain. Central to this thesis is the isomorphism that reveals the precise extent to which these polyhedra can represent dependency information. An argument-size analysis using polyhedra and a groundness analysis using certain polyhedral cones have been implemented up to the prototype stage.