On the Use of Tabling for Abstract Interpretation: An Experiment with Abstract Equation Systems

Click on the title to obtain a gzip-ed PostScript version of the paper (50K).


Abstract:

Abstract interpretation is a widely used method for the static analysis of programs. This paper reports on our recent experiments with an alternative approach to implementing program analyses based on abstract interpretation. Instead of using a special-purpose system for abstract interpretation (such as PLAI, GAIA, or AMAI), we follow the approach advocated in the paper which you can access by clicking here and use a logic programming system which supports tabling (namely XSB). To obtain the results of the analysis, we directly compile the program to be analysed into a tabled logic program such that its execution by XSB coincides with the abstract interpretation of the original program. We show how this approach is adapted to abstractions which satisfy the requirements of the framework of Bruynooghe and that the approach is practical and competitive with state-of-the-art generic abstract interpretation systems implemented in Prolog. Our experiments are based on the non-trivial domain of abstract equation systems which is a parameterized domain which captures structure information together with modes, linearity and sharing.