School Homepage

Papers of Patricia M. Hill

Software Support for CLP: Papers

Technical Reports at Leeds

Abstract Domains for Universal and Existential Properties

[Page last updated on 2000/10/25.]

Andrew Heaton
School of Computing
The University of Leeds
Leeds LS2 9JT
England

Patricia M. Hill
School of Computing
The University of Leeds
Leeds LS2 9JT
England

Andy King
Computing Laboratory
The University of Kent at Canterbury
Canterbury CT2 7NF
England

Abstract:

Abstract interpretation theory has successfully been used for constructing algorithms to statically determine run-time properties of programs. Central is the notion of an abstract domain, describing certain properties of interest about the program. In logic programming, program analyses typically fall into two different categories: either they detect program points where the property definitely holds (universal analyses) or possibly holds (existential analyses). We study the relation between such analyses in the case where the concrete domain is a lattice join-generated by its set of join-irreducible elements. Although our intended application is for logic programming, the theory is sufficiently general for possible applications to other languages.

In:

Proceedings of European Symposium on Programming (ESOP 2000), LNCS, Springer-Verlag

Available: PS and BibTeX entry.