Click on the title to obtain a gzip-ed PostScript version
of a paper almost identical to the journal version (92K).
Abstract:
This article describes a simple and efficient way of using a logic
programming language with builtin tabulation for general purpose
semantics-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, our approach using 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
techniques and optimizations of other frameworks in a straightforward
and flexible way.