Predicate abstraction and canonical abstraction are two finitary abstractions
used to prove properties of programs. We study the relationship between these
two abstractions by considering a very limited case: abstraction of
(potentially cyclic) singly-linked lists.
We provide a new and rather precise family of abstractions for
potentially cyclic singly-linked lists. The main observation
behind this family of abstractions is that the number of shared
nodes in linked lists can be statically bounded. Therefore, the
number of possible ``heap shapes'' is also bounded.
We present the new abstraction in both predicate abstraction form as well as
in canonical abstraction form.
As we illustrate in the paper, given any canonical abstraction, it is possible
to define a predicate abstraction that is equivalent to the canonical
abstraction. However, with this straightforward simulation, the number of
predicates used for the predicate abstraction is exponential in the number of
predicates used by the canonical abstraction.
An important feature of the family of abstractions we present in this paper is
that the predicate abstraction representation we define is far more practical
as it uses a number of predicates that is quadratic in the number of
predicates used by the corresponding canonical abstraction representation.
In particular, for the most abstract abstraction in this family,
the number of predicates used by the canonical abstraction is linear in the
number of program variables, while the number of predicates used by the
predicate abstraction is quadratic in the number of program variables.
We have encoded this particular predicate abstraction and
corresponding transformers in TVLA, and used this implementation
to successfully verify safety properties of several list
manipulating programs, including programs that were not previously
verified using predicate abstraction or canonical abstraction.