In earlier work, we presented an abstraction-refinement mechanism that was successful in verifying automatically the partial correctness of in-situ list reversal when applied to an acyclic linked list. This paper reports on the automatic verification of the total correctness (partial correctness and termination) of the same list-reversal algorithm, when applied to a possibly-cyclic linked list. A key contribution that made this result possible is an extension of the finite-differencing technique to enable the maintenance of reachability information for a restricted class of possibly-cyclic data structures, which includes possibly-cyclic linked lists.

(Click here to access the paper: PDF; (c) Springer-Verlag.)