Skip to main content
Kent Academic Repository

Polyhedral domains for abstract interpretation in logic programming

Benoy, Patricia Mary (2002) Polyhedral domains for abstract interpretation in logic programming. Doctor of Philosophy (PhD) thesis, University of Kent. (doi:10.22024/UniKent/01.02.86251) (KAR id:86251)


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.

Item Type: Thesis (Doctor of Philosophy (PhD))
Thesis advisor: King, Andy
DOI/Identification number: 10.22024/UniKent/01.02.86251
Additional information: This thesis has been digitised by EThOS, the British Library digitisation service, for purposes of preservation and dissemination. It was uploaded to KAR on 09 February 2021 in order to hold its content and record within University of Kent systems. It is available Open Access using a Creative Commons Attribution, Non-commercial, No Derivatives ( licence so that the thesis and its author, can benefit from opportunities for increased readership and citation. This was done in line with University of Kent policies ( If you feel that your rights are compromised by open access to this thesis, or if you would like more information about its availability, please contact us at and we will seriously consider your claim under the terms of our Take-Down Policy (
Uncontrolled keywords: Software, computer programming
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
SWORD Depositor: SWORD Copy
Depositing User: SWORD Copy
Date Deposited: 29 Oct 2019 16:38 UTC
Last Modified: 16 Dec 2021 10:47 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.