Refinement-based verification for possibly-cyclic lists

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 [10]. This paper reports on the automatic verification of the total correctness (partial correctness and termination) of the same list-reversal algorithm, when applied to apossibly-cyclic linked list. A key contribution that made this result possible is an extension of the finite differencing technique [14] to enable the maintenance of reachability information for a restricted class of possibly-cyclic data structures, which includes possiblycyclic linked lists.