Using XSB for Abstract Interpretation

David S. Warren, Steven Dawson, C. R. Ramakrishnan


Abstract:

XSB is a tabling Prolog system. In addition to Prolog's usual SLD, XSB supports SLG resolution, which can be understood as an extension of OLDT resolution to handle negation under the well-founded semantics. SLG terminates for all Horn programs with the bounded term size property, in particular for those with a finite Herbrand Base. This property makes XSB usable as a tool for implementing abstract interpreters. In this paper, we describe our experience with constructing abstract interpreters using XSB. We find that it is straightforward to obtain simple yet practical implementations of analyses using XSB. Our experiments also suggest a number of enhancements to the system that will improve performance as well as the ease of implementing AI in XSB.


Bibtex Entry:

@inproceedings{WDR:WAILL95,
author = {David S. Warren and  Steven Dawson and  C. R. Ramakrishnan},
title = {Using {XSB} for Abstract Interpretation},
booktitle = {Special Workshop on Abstract Interpretation of Logic Languages},
address = {Eilat, Israel},
year = {1995}
}


Full Paper: [pdf]


Home | Papers

C. R. Ramakrishnan
(cram@cs.sunysb.edu)