Refinement-Based Verification for Possibly-Cyclic Lists
Alexey Loginov, Thomas Reps, and Mooly Sagiv
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.)