Michael Codish

Groundness analysis of logic programs using Pos-based abstract interpretation is one of the clear success stories of the last decade in the area of logic program analysis. In this work we identify two problems with the Pos domain, the multiplicity and sign problems, that arise independently in groundness and uniqueness analysis. We describe how these problems can be solved using an analysis based on a domain Size for inferring term size relations. However this solution has its own shortcomings because it involves a widening operator which leads to a loss of Pos information. Inspired by Pos, Size and the LSign domain for abstract linear arithmetic constraints we introduce a new domain LPos, and show how it can be used for groundness and uniqueness analysis. The idea is to use the sign information of LSign to improve the widening of Size so that it does not lose Pos information. We prove that the resulting analyses using LPos are uniformly more precise than those using Pos.