The impact of granularity in abstract interpretation of prolog

Abstract

Abstract interpretation of Prolog has received much attention in recent years leading to the development of many frameworks and algorithms. One reason for this proliferation comes from the fact that program analyses can be defined at various granularities, achieving a different trade-off between efficiency and precision. The purpose of this paper is to study this tradeoff experimentally. We review the most frequently proposed granularities which can be expressed as a two dimensional space parametrized by the form of the inputs and outputs. The resulting algorithms are evaluated on three abstract domains with very different functionalities, Mode, Prop, and Pattern to assess the impact of granularity on efficiency and accuracy. This is, to our knowledge, the first study of granularity at the algorithm level and some of the results are particularly surprising.