Semantic-Based Program Analysis for Logic-Based Languages using XSB

Michael Codish, Bart Demoen and Kostis Sagonas

Springer International Journal of Software Tools for Technology Transfer; 2 (1): 29-45, 1998

Abstract:

This paper describes a simple and efficient way of using a logic programming language with tabulation for general purpose semantic-based program analysis. The simplicity of the method is based on a clear separation of abstraction and control: conceptually, a concrete program is executed over an abstract domain and the tabulation mechanism avoids recomputation, ensures termination and collects the results of the analysis. The efficiency derives from the fact that an abstract interpreter induces an abstract compiler which maps input programs to corresponding abstract programs which are (compiled and) run in XSB. The design of new analyses is an easy and fast process, because XSB is a general purpose logic programming system which supports efficient fix-point computations through tabling implemented at the abstract machine level and comes off the shelf: in fact, due to its optimized control and superior tabling performance, XSB competitively compares with most of the existing special purpose abstract interpretation tools for logic programs. We demonstrate that our approach to using XSB for abstract interpretation supports the usual optimisations of other frameworks in a straightforward and very flexible way.

Available: bibtex entry compressed postscript

Related sites: PDF from the publisher

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il