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 a possibly-cyclic linked list. A key contribution that made this result possible is an extension of the finitedifferencing technique [14] to enable the maintenance of reachability information for a restricted class of possibly-cyclic data structures, which includes possiblycyclic linked lists.

• Type: Conference
• Year: 2006
• Where: BIRTHDAY
• Authors: Alexey Loginov, Thomas W. Reps, Mooly Sagiv
• Keywords: Acyclic Linked List, Applied Computing, BIRTHDAY 2006, Linked Lists, Partial Correctness