© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Abstract Domains for Universal and Existential Properties
A. Heaton, P. Hill, and A. King
In G. Smolka, editor, European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, March 2000 see http://www.springer.de./comp/lncs/index.html.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.
Download publication 193 kbytes (PostScript)Bibtex Record
@inproceedings{956,
author = {A.~Heaton and P.~Hill and A.~King},
title = {Abstract {D}omains for {U}niversal and {E}xistential {P}roperties},
month = {March},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {see http://www.springer.de./comp/lncs/index.html},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/956},
booktitle = {European Symposium on Programming},
editor = {G. Smolka},
publication_type = {inproceedings},
publisher = {Springer-Verlag},
submission_id = {6385_947861999},
series = {Lecture Notes in Computer Science},
volume = {1782},
}